Automatically synthesizing consistent models is a key prerequisite for many testing
scenarios in autonomous driving to ensure a designated coverage of critical corner
cases. An inconsistent model is irrelevant as a test case (e.g., false positive);
thus, each synthetic model needs to simultaneously satisfy various structural and
attribute constraints, which includes complex geometric constraints for traffic scenarios.
While different logic solvers or dedicated graph solvers have recently been developed,
they fail to handle either structural or attribute constraints in a scalable way.
In the current paper, we combine a structural graph solver that uses partial models
with an SMT-solver and a quadratic solver to automatically derive models which simultaneously
fulfill structural and numeric constraints, while key theoretical properties of model
generation like completeness or diversity are still ensured. This necessitates a sophisticated
bidirectional interaction between different solvers which carry out consistency checks,
decision, unit propagation, concretization steps. Additionally, we introduce custom
exploration strategies to speed up model generation. We evaluate the scalability and
diversity of our approach, as well as the influence of customizations, in the context
of four complex case studies.
