Name
Abstract | ||
|---|---|---|
We present a unifying framework for understanding and developing SAT-based decision pro- cedures for Satisabilit y 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 identied as special cases. This framework oers the rst generic approach for eager encodings, and a simple generalization of various lazy techniques that are found in the literature. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/s00165-009-0105-z | Formal Asp. Comput. |
Keywords | Field | DocType |
decision problem,sat solver,satisfiability modulo theories,propositional logic | Discrete mathematics,Decision problem,Computer science,Boolean satisfiability problem,Propositional calculus,Theoretical computer science,DPLL algorithm,Decision theory,Satisfiability modulo theories | Journal |
Volume | Issue | ISSN |
21 | 5 | 1433-299X |
Citations | PageRank | References |
3 | 0.40 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Kroening | 1 | 3084 | 187.60 |
| Ofer Strichman | 2 | 1071 | 63.61 |