Splitting on demand in SAT Modulo theories

Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings
Pages512-526
Number of pages15
Volume4246 LNAI
StatePublished - 2006
Event13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006 - Phnom Penh, Cambodia
Duration: Nov 13 2006Nov 17 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4246 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006
CountryCambodia
CityPhnom Penh
Period11/13/0611/17/06

Fingerprint

Modulo
Engines
Engine
Demand
Internal
Delegation
Reasoning
Modeling

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Barrett, C., Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Splitting on demand in SAT Modulo theories. In Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings (Vol. 4246 LNAI, pp. 512-526). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4246 LNAI).

Splitting on demand in SAT Modulo theories. / Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare.

Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. Vol. 4246 LNAI 2006. p. 512-526 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4246 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Barrett, C, Nieuwenhuis, R, Oliveras, A & Tinelli, C 2006, Splitting on demand in SAT Modulo theories. in Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. vol. 4246 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4246 LNAI, pp. 512-526, 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, Phnom Penh, Cambodia, 11/13/06.
Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C. Splitting on demand in SAT Modulo theories. In Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. Vol. 4246 LNAI. 2006. p. 512-526. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Barrett, Clark ; Nieuwenhuis, Robert ; Oliveras, Albert ; Tinelli, Cesare. / Splitting on demand in SAT Modulo theories. Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings. Vol. 4246 LNAI 2006. pp. 512-526 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{eabcebdbae354135a99101dc8fbeed66,
title = "Splitting on demand in SAT Modulo theories",
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.",
author = "Clark Barrett and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli",
year = "2006",
language = "English (US)",
isbn = "3540482814",
volume = "4246 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "512--526",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings",

}

TY - GEN

T1 - Splitting on demand in SAT Modulo theories

AU - Barrett, Clark

AU - Nieuwenhuis, Robert

AU - Oliveras, Albert

AU - Tinelli, Cesare

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33845215878&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845215878&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:33845215878

SN - 3540482814

SN - 9783540482819

VL - 4246 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 512

EP - 526

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 13th International Conference, LPAR 2006, Proceedings

ER -