1. SMT
SMT is an abbreviation of Satisfiability Modulo Theories. The SMT problem is a decision problem for formulas with respect to theories expressed in classical first-order logic with equality.
For example, a > 10 is a formula. Is this True or False? Obviously, we cannot answer this because it is neither True or False. The truth of the formula depends on what a is. Therefore, a question better than the previous one here is whether or not the formula is satisfiable. If it is so, we may be curious about when it is satisfiable, in other words, what is a model for the formula. An answer is that the formula is satisfiable when a is 11. An SMT solver will produce this kind of answer automatically.
The SMT problem is a combination of the boolean satisfiability problem (SAT) with an arbitrary theory. In the above example, we had SAT with an integer arithmetic theory. To solve the above example, it is not difficult to imagine that we need to use both a SAT solver and a decision procedure in Linear algebra such as the simplex algorithm. Another example formula may be (a and ((x + y <= 0) or not a) and ((x = 1) or b), which may explain better the necessity of the two solvers.
2. OpenSMT
The OpenSMT is an effort to build an SMT solver under the open source policy. This contrasts to most of the other SMT solvers, which are proprietary, such as Z3.
The OpenSMT provides a SAT solver, which is based on another cool open source MiniSAT, and it supports several theories including QF_UF, QF_IDL, QF_RDL, QF_LRA, QF_BV, F_UFIDL, and QF_UFLRA. For example, QF_UFLRA is a theory combination of uninterpreted functions and linear arithmetic on the rationals.
The OpenSMT combines each pair of the SAT solver and a decision procedure on one of the theories using DPLL framework. The DPLL algorithm is a complete, backgracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e., for solving the CNF-SAT problem. (DPLL denotes the names of early scientists Martin Davis, Hilary Putnam, George Logemann and Donald W. Loveland.)
The OpenSMT offers a set of C++ APIs to extend itself with a decision procedure on a theory. The theories mentioned above are integrated using those APIs. This way the OpenSMT opens its architecture to everyone and every theory.
The OpenSMT is capable of computing models and proofs. In case of formulas in SAT, it computes assignments to satisfy them to be True. It prints models in SMT-LIB syntax such as (= x 1) and (not b). It also prints models in the resolution proof format, which can guide a proof to lead to True. Given an unsatisfiable conjunction, the OpenSMT is able to generate a sequence of inferences that lead to a contradiction.
No comments:
Post a Comment