Lemmas on Demand for Satisfiability Solvers

In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT'02.
Authors
Leonardo de Moura and Harald Rueß
Abstract
We investigate the combination of propositional SAT checkers with satisfiability procedures for domain-specific theories such as linear arithmetic, arrays, lists and the combination thereof. Our procedure realizes a lazy approach to satisfiability checking of Boolean constraint formulas by iteratively refining Boolean formulas based on lemmas generated on demand by the decision procedures.
Download: PS, PDF
Download (extended version): PS, PDF
BibTeX Entry 
@inproceedings{dMR:SAT'2002,
  TITLE = {Lazy Theorem Proving for Bounded Model Checking over Infinite Domains},
  AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and Maria Sorea},
  YEAR = 2002,
  BOOKTITLE="Proceedings of the Fifth International Symposium on the
             Theory and Applications of Satisfiability Testing (SAT'02)",
}
Leonardo de Moura: demoura@csl.sri.com