Satisfiability modulo Theories. Barrett, C.; Sebastiani, R.; Seshia, S. A.; and Tinelli, C. 185(1):825–885.
doi  abstract   bibtex   
We present a unifying framework for understanding and developing SAT-based decision procedures for Satisfiability Modulo Theories (SMT). The framework is based on a reduction of the decision problem to propositional logic by means of a deductive system. The two commonly used techniques, eager encodings (a direct reduction to propositional logic) and lazy encodings (a family of techniques based on an interplay between a SAT solver and a decision procedure) are identified as special cases. This framework offers the first generic approach for eager encodings, and a simple generalization of various lazy techniques that are found in the literature.
@article{barrettSatisfiabilityModuloTheories2009,
  title = {Satisfiability modulo Theories},
  volume = {185},
  issn = {09226389},
  doi = {10.3233/978-1-58603-929-5-825},
  abstract = {We present a unifying framework for understanding and developing SAT-based decision procedures for Satisfiability Modulo Theories (SMT). The framework is based on a reduction of the decision problem to propositional logic by means of a deductive system. The two commonly used techniques, eager encodings (a direct reduction to propositional logic) and lazy encodings (a family of techniques based on an interplay between a SAT solver and a decision procedure) are identified as special cases. This framework offers the first generic approach for eager encodings, and a simple generalization of various lazy techniques that are found in the literature.},
  number = {1},
  journaltitle = {Frontiers in Artificial Intelligence and Applications},
  date = {2009},
  pages = {825--885},
  author = {Barrett, Clark and Sebastiani, Roberto and Seshia, Sanjit A. and Tinelli, Cesare},
  file = {/home/dimitri/Nextcloud/Zotero/storage/J6SFG3SZ/SATChapter12.pdf}
}
Downloads: 0