A framework for Satisfiability Modulo Theories |
| |
Authors: | Daniel Kroening Ofer Strichman |
| |
Affiliation: | 1. Computing Laboratory, Oxford University, Oxford, UK 2. Information Systems Engineering, IE, Technion, 32000, Haifa, Israel
|
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|