Ways to think formally about Satisfiability Modulo Theories

Question

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?

Answer 1

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).