Turbo-Charging Lemmas on Demand with Don't Care Reasoning
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
FMCAD 2014
Sprache des Tagungstitel:
Englisch
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 enhanc-
ing lemmas on demand with don?t care reasoning, the number
of lemmas generated, and consequently the solver runtime, is
reduced considerably.