Splitting on Demand in SAT Modulo Theories

Splitting on Demand in SAT Modulo Theories” by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. In Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), (Miki Hermann and Andrei Voronkov, eds.), Nov. 2006, pp. 512-526. Phnom Penh, Cambodia.

Abstract

Lazy algorithms for Satisfiability Modulo Theories (SMT) combine a generic DPLL-based SAT engine with a theory solver for the given theory T that can decide the T-consistency of conjunctions of ground literals. For many theories of interest, theory solvers need to reason by performing internal case splits. Here we argue that it is more convenient to delegate these case splits to the DPLL engine instead. The delegation can be done on demand for solvers that can encode their internal case splits into one or more clauses, possibly including new constants and literals. This results in drastically simpler theory solvers. We present this idea in an improved version of DPLL(T), a general SMT architecture for the lazy approach, and formalize and prove it correct in an extension of Abstract DPLL Modulo Theories, a framework for modeling and reasoning about lazy algorithms for SMT. A remarkable additional feature of the architecture, also discussed in the paper, is that it naturally includes an efficient Nelson-Oppen-like combination of multiple theories and their solvers.

BibTeX entry:

@inproceedings{BNO+06,
   author = {Clark Barrett and Robert Nieuwenhuis and Albert Oliveras and
	Cesare Tinelli},
   editor = {Miki Hermann and Andrei Voronkov},
   title = {Splitting on Demand in {SAT} Modulo Theories},
   booktitle = {Proceedings of the {\it 13^{th}} International Conference
	on Logic for Programming, Artificial Intelligence, and Reasoning
	(LPAR '06)},
   series = {Lecture Notes in Computer Science},
   volume = {4246},
   pages = {512--526},
   publisher = {Springer-Verlag},
   month = nov,
   year = {2006},
   note = {Phnom Penh, Cambodia},
   url = {http://theory.stanford.edu/~barrett/pubs/BNO+06.pdf}
}

(This webpage was created with bibtex2web.)