Lemmas on Demand for Satisfiability Solvers

---

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.

gzipped postscript or postscript Extended version has been accepted for publication in the Annals of Mathematics and Artificial Intelligence (AMAI).

BibTeX Entry

@unpublished{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,
        MONTH = {May}, 
	NOTE = {Presented at the Fifth International
                Symposium on the Theory and Applications of Satisfiability Testing (SAT'02),
                Cincinnati, USA, 15 May 2002}
}

(an extended version is submitted for publication.)

---

Harald Ruess: ruess@csl.sri.com