Satisfiability modulo Theories. Barrett, C., Sebastiani, R., Seshia, S. A., & 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
{"_id":"zTWdwPzn6FBKMrdDd","bibbaseid":"barrett-sebastiani-seshia-tinelli-satisfiabilitymodulotheories","downloads":0,"creationDate":"2016-08-22T10:51:33.899Z","title":"Satisfiability modulo Theories","author_short":["Barrett, C.","Sebastiani, R.","Seshia, S. A.","Tinelli, C."],"year":null,"bibtype":"article","biburl":"https://raw.githubusercontent.com/dlozeve/newblog/master/bib/all.bib","bibdata":{"bibtype":"article","type":"article","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":[{"propositions":[],"lastnames":["Barrett"],"firstnames":["Clark"],"suffixes":[]},{"propositions":[],"lastnames":["Sebastiani"],"firstnames":["Roberto"],"suffixes":[]},{"propositions":[],"lastnames":["Seshia"],"firstnames":["Sanjit","A."],"suffixes":[]},{"propositions":[],"lastnames":["Tinelli"],"firstnames":["Cesare"],"suffixes":[]}],"file":"/home/dimitri/Nextcloud/Zotero/storage/J6SFG3SZ/SATChapter12.pdf","bibtex":"@article{barrettSatisfiabilityModuloTheories2009,\n title = {Satisfiability modulo Theories},\n volume = {185},\n issn = {09226389},\n doi = {10.3233/978-1-58603-929-5-825},\n 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.},\n number = {1},\n journaltitle = {Frontiers in Artificial Intelligence and Applications},\n date = {2009},\n pages = {825--885},\n author = {Barrett, Clark and Sebastiani, Roberto and Seshia, Sanjit A. and Tinelli, Cesare},\n file = {/home/dimitri/Nextcloud/Zotero/storage/J6SFG3SZ/SATChapter12.pdf}\n}\n\n","author_short":["Barrett, C.","Sebastiani, R.","Seshia, S. A.","Tinelli, C."],"key":"barrettSatisfiabilityModuloTheories2009","id":"barrettSatisfiabilityModuloTheories2009","bibbaseid":"barrett-sebastiani-seshia-tinelli-satisfiabilitymodulotheories","role":"author","urls":{},"downloads":0},"search_terms":["satisfiability","modulo","theories","barrett","sebastiani","seshia","tinelli"],"keywords":[],"authorIDs":[],"dataSources":["3XqdvqRE7zuX4cm8m"]}