6
$\begingroup$

Apologies if this is not a well-thought-out question, but I am interested in formalizing a problem which is ultimately described by a SMT formula in the theory of quantified arrays and linear arithmetic, and I realized that, while I understand what SMT formulas are useful for in a practical sense, I do not have a good sense for how to fit what I know about foundations of logic/computing/type theory/category theory with the idea of SMT theories and formulas. What can be said formally about the general theory about statements which can in some way be turned into SAT instances?

Edit: I understand that SAT solvers work with propositional logic and SMT solvers work with fragments of first-order logic, but how exactly do we understand what a "fragment of logic" is and how it chops up the whole universe of first-order logic? Obviously we have different predicates and functions for linear arithmetic vs the theory of data types, but how at a formal level can we come up with a mathematical universe in which certain statements can be combined and others can't?

$\endgroup$
  • $\begingroup$ It's somewhat unclear what you are asking. SAT typically referes to propositional satisfiability. SMT heavily depends on the theories one considers. E.g. do you need quantifiers? If so, how many alternations? Typically a particular theory represents a fragment of first order logic (this fragment may or may not be decidable). $\endgroup$ – Mikolas May 3 '18 at 21:13
  • $\begingroup$ Edited for clarity - does this make more sense? $\endgroup$ – lightning May 3 '18 at 22:25
  • 1
    $\begingroup$ A FOL theory is simply a set of FOL axioms. Combining theories means taking the union of the axioms. The difficult part is how to combine the accompanying decision procedures, which are specialized for particular theories. For that, see either the original Nelson--Oppen, or something newer like DPLL(T). The basic idea is to start with a SAT solver, and hang other decision procedures on it, while communicating only formulas of a certain shape (equalities). $\endgroup$ – Radu GRIGore May 4 '18 at 5:05
6
$\begingroup$

It's actually surprisingly hard to relate SMT to type-theoretic/categorical approaches to logic -- the results in this area are very recent! This is because categorical logic is primarily conceived of as a semantics of proofs, and SMT arises from the model-theoretic view of logic, which is a semantics of provability.

A formula in SMT is a boolean combination of primitive assertions over some theory. For example, for linear arithmetic you might have the following terms and primitive formulas.

$$ \newcommand{\bnfalt}{\;\;|\;\;} \array{ \mbox{Terms} & t & ::= & x \bnfalt n \bnfalt t + t \bnfalt -t \\ \mbox{Primitive Formulas} & p & ::= & t \leq t \bnfalt t = t \bnfalt t < t \\ \mbox{SMT Formulas} & \phi & ::= & p \bnfalt \top \bnfalt \phi \land \phi' \bnfalt \lnot \phi \\ }$$

Given a formula $\phi$, an SMT solver will either give you a satisfying assignment for the variables -- i.e., it will give you a number for each variable, such that substituting that number for each variable gives you a true boolean formula -- or it will tell you that the formula $\phi$ is unsatisfiable.

The fact that this is all happening in classical logic is quite important; the architecture of SMT solvers relies upon this fact. Basically, SMT solvers are built as a combination of an DPLL-based SAT solver, which communicates with a theory solver, which deduces equalities from pure conjunctions of theory formulas. There are also various conditions under which you can combine solvers for different theories, which is important because it gives researchers a good "API" for figuring out if particular theories will fit together nicely.

A good reference to the standard view of SMT is Clark Barrett and Cesare Tinelli's handbook chapter on Satisfiability Modulo Theories.

Work on how to interpret SMT in terms of proof theory is much newer. The basic idea is to relate DPLL(T) with "focused" or "polarized" calculi for proof search. Focused calculi are variants of the sequent calculus originally designed to optimize proof search, but which turned out to work because they expose fundamental ideas in proof theory.

Two good references to this are Mahfuza Farooque's PhD thesis, Automated reasoning techniques as proof-search in sequent calculus, in which she relates the actions of a DPLL(T) algorithm to search in a particular focused calculus, and Stéphane Graham-Lengrand's habilitation thesis Polarities & Focussing: a journey from Realisability to Automated Reasoning, in which he gives a broader perspective on this work (eg, by connecting it to work on biorthogonality).

$\endgroup$
  • 2
    $\begingroup$ SMT doesn't really have anything to do with DPLL as such, you could do SMT solving with other approaches to SAT solving. The key idea is simply how the SAT and theory solvers interact. In practise most high-performance SAT solvers are descending from DPLL, albeit just how much DPLL is still in modern CDCL solvers is debatable. $\endgroup$ – Martin Berger May 4 '18 at 13:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.