Aina Niemetz, Mathias Preiner, Armin Biere,
"Turbo-Charging Lemmas on Demand with Don't Care Reasoning"
: Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), FMCAD Inc., Seite(n) 179-186, 2014
Original Titel:
Turbo-Charging Lemmas on Demand with Don't Care Reasoning
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14)
Original Kurzfassung:
Lemmas on demand is an abstraction/refinement
technique for procedures deciding Satisfiability Modulo Theories
(SMT), which iteratively refines full candidate models of the
formula abstraction until convergence. In this paper, we introduce
a dual propagation-based technique for optimizing lemmas on
demand by extracting partial candidate models via don?t care
reasoning on full candidate models. Further, we compare our
approach to a justification-based approach similar to techniques
employed in the context of model checking. We implemented
both optimizations in our SMT solver Boolector and provide an
extensive experimental evaluation, which shows that by enhancing
lemmas on demand with don?t care reasoning, the number
of lemmas generated, and consequently the solver runtime, is
reduced considerably.