Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical problem instances with millions of variables and clauses. This efficiency of solvers is in surprising contrast to the traditional complexity theory position that the problems that these solvers address are believed to be hard in the worst case. In an attempt to resolve this apparent discrepancy between theory and practice, theorists have proposed the study of these solvers as proof systems that would enable establishing appropriate lower and upper bounds on their complexity. For example, in recent years it has been shown that (idealized models of) SAT solvers are polynomially equivalent to the general resolution proof system for propositional logic, and SMT solvers that use the CDCL(T) architecture are polynomially equivalent to the Res * (T) proof system.
In this paper, we extend this program to the MCSAT approach for SMT solving by showing that the MCSAT architecture is polynomially equivalent to the Res * (T) proof system. Thus, we establish an equivalence between CDCL(T) and MCSAT from a proof-complexity theoretic point of view. This is a first and essential step towards a richer theory that may help (parametrically) characterize the kinds of formulas for which MCSAT-based SMT solvers can perform well.
In this work we are interested in proof systems to decide the satisfiability of (quantifier-free first-order logic) formulas. Well-known proof systems include variants of the resolution proof system for propositional logic, but also for first-order logic as presented in [RKG]. An interesting measure to compare proof systems is their proof complexity: if we can show that in a proof system we can generate shorter proofs (with less proof steps) than in another, we consider the former proof system more powerful.
One particular problem that concerns quantifier-free first-order logic formulas is to determine their satisfiability. Answering this question (at least for certain theories) has spawned an active field of research called satisfiability modulo theories (SMT) solving [BHvMW09,KS08]. The predominant approach is called CDCL(T) and works by combining a solver for propositional logic (a SAT solver ) with a solver that checks a set of theory constraints for consistency (a theory solver ).
A significantly different solving technique called MCSAT was presented in [JdM, dMJ] which provides a significantly tighter integration of the Boolean and the theory reasoning. This solver performs extremely well in practice, at least for "hard" theories like non-linear real arithmetic, thus naturally raising the question whether this MCSAT implementation only happens to include better heuristics, or whether MCSAT itself has some more fundamental advantage over CDCL (T).
We tackle this question from the perspective of proof complexity, allowing us to abstract from certain practical aspects very naturally, for example the impact of heuristics. We can understand both CDCL(T) and MCSAT as proof systems [NOT06,dMJ]. The proof complexity of CDCL(T) was found in [RKG] to be equivalent to the Res * (T) proof system. In this paper, we show that also the MCSAT architecture is polynomially equivalent to the Res * (T) proof system. Thus, we establish an equivalence between CDCL(T) and MCSAT from a complexitytheoretic view.
It is important to realize, that there is a subtle but important difference between what we call DPLLreferring to the original DPLL method from [DLL62] -and the version extended with clause learning -proposed in [MS] -that we now call CDCL. Compared to CDCL(T) (and Res * (T)), DPLL(T) is weaker in terms of proof complexity and we only argue about CDCL(T) throughout this paper.
We assume the reader to be familiar with deductive proof systems and give in the following just a short introduction to notation. For readability, in the following we will use conditional proof rules of the form
to form proof systems. Such a rule with name PR allows to derive the consequent C from the antecedents A 1 , . . . , A n and some side conditions S 1 , . . . , S m . We will typically describe some state in a single antecedent A and some conditions on this state in S 1 , . . . , S m . Note that the above conditional proof rule is equivalent to one without side-condition but with the antecedents A 1 , . . . , A n , S 1 , . . . , S m . A (deductive) proof system is a set of such (conditional) proof rules. By a derivability statement Γ C we denote that we can prove C from a set Γ of antecedents (and side conditions), i.e., that C is derivable from Γ by finitely many proof rule applications. By Γ |= C we denote that Γ assures the truth of C (with respect to an underlying semantics). Qualitative properties of proof systems include soundness (if Γ C then Γ |= C) and completeness (if Γ |= C then Γ C). All the proof systems that we consider in this paper are sound and complete; we refer to the respective references for details.
The length of a proof in a proof system is the number of proof rule applications used in it; a proof is shorter then another one if its length is smaller. The proof complexity for Γ C is the length of the shortest proof that derives C from Γ. Our aim in this paper is to compare for certain classes of derivability statements their proof complexities in different proof systems.
Assume two proof systems P 1 and P 2 , and a metric to measure the size of derivability statements that are true in both systems. We say that P 1 is more powerful than P 2 on a set of such statements if the proof complexity grows (at most) polynomially with the statement (input) size in P 1 but exponentially in P 2 . We call P 1 and P 2 comparable if one of them is more powerful than the other on all such classes, and incomparable otherwise. We refer to [RKG] for a discussion of existing proof systems and their relations in terms of proof complexity.
In the following we recall the MCSAT proof system for the satisfiability check of quantifier-free first-order logic formulas as defined in [dMJ]. Following [dMJ], we present the proof rules in three categories: Boolean reasoning (fig. 1), conflict analysis (fig. 2) and theory reasoning (fig. 3). The Boolean reasoning and conflict analysis parts essentially constitute a regular CDCL-style SAT solver while the theory reasoning part enhances the proof system to allow for SMT-style theory computations.
Decide: The only modification to [dMJ] is the addition of the Restart rule (fig. 1), which is sound and also does not introduce non-termination as long as we ensure that it is applied with increasing periodicity [NOT06]. Restarts are a standard technique both in CDCL-style SAT solving and in SMT solving, but such a rule was not included in the original MCSAT proof system. However, we will need this rule for the proof complexity results in the next section.
Due to space restrictions, in the following we discuss the rules only briefly and refer to [dMJ] for more detailed explanations.
The proof system works on states of the form M, C consisting of a trail M and a set C of clauses whose satisfaction we are interested in, where the literals of the clauses are constraints from a given theory T . The trail is a list of Boolean decisions, theory decisions, Boolean propagations and theory propagations. Decisions represent exploration by enumeration: a Boolean decision L assigns the Boolean value true to the literal L (fig. 1, rule Decide; the Basis set and the value function will be explained a bit later), whereas a theory decision x → α x assigns the theory value α x to the theory variable x (fig. 3, rule T-Decide; consistency of a trail is explained below). A Boolean propagation C → L states that the satisfaction of C under previous decisions is possible only if L is true with the reason being the clause C (fig. 1, rule Propagate). Analogously, a theory propagation E → L states an implication based on a lemma, i.e. a tautology in the theory (T-Propagate, fig. 3). We write M 1 , . . . , M k to explicitly denote individual elements of the trail, and we call a trail complete if it assigns a Boolean value to each variable or its negation (either by Boolean decision or propagation) as well as a theory value to each theory variable. Satisfiability of a CNF formula can be proven by deriving the SAT state, based on a complete trail that satisfies each clause (fig. 1, rule Sat).
For theory variables x, if there is some theory value α x such that x → α x is in the trail M then the value value(x, M ) of a theory variable x in trail M is α x , and undef otherwise.
A literal L, which is either a theory constraint c or the negation ¬c of a constraint c, can be evaluated by two semantics: c or ¬c can enter the trail by Boolean decision or propagation, but also the theory variables in c can be assigned a value from the theory domain. The proof system argues in both the Boolean and the theory domain concurrently, but it assures that they stay consistent, meaning that the Boolean and the theory evaluation of a constraint never contradict. Thus the value value(L, M ) of a literal L in a trail M is true if L is decided or propagated in M , or if L evaluates to true when we substitute the theory values from M in L; it is false if ¬L is decided or propagated in M , or if L evaluates to false under the theory assignments; and undef otherwise. We call a consistent trail M feasible if the trail's theory variable assignments can be extended to satisfy all clauses C ∈ C with value(C, M ) = true; by infeasible(M ) we denote that M is not feasible.
From a search state M, C we enter the conflict state M, C C when a violated conflict clause (i.e., a clause whose literals all evaluate to false under the current trail M ) is detected (fig. 1, rule Conflict), or the conflict state M, C E when the trail is infeasible and E is a theory lemma explaining this fact. The Resolve: The explain function explains theory-specific propagations and infeasible states. The proof systems assumes the existence of a finite set Basis of theory constraints such that all literals from all clauses, especially those returned by the explain function, are contained in it. The finiteness provides a nice termination argument as only finitely many (different) clauses exist. Also explanations can be learned and forgotten (rules Learn in fig. 2 and Forget in fig. 1).
Our reference proof system is (one of the variants of) the resolution proof system. Two resolution proof systems for first-order logic with some theory T called Res(T) and Res * (T) are discussed in [RKG]. They enhance the traditional resolution proof system for propositional logic by a proof rule that allows for the introduction of new clauses that state tautologies from the theory. While Res * (T) allows for strong theory derivation which may also introduce new literals (theory constraints), Res(T) is restricted to (regular) theory derivation that allows only literals that occur in the formula already.
Introducing new literals can make a significant difference for certain problem classes as discussed in [RKG]. As the MCSAT proof system may as well introduce new literals -the explain method makes heavy use of this in many cases -we use Res * (T) for the following comparison, consisting of the Resolution rule and the Strong Theory Derivation rule.
Note that these proof systems lack dedicated final states -like SAT and UNSAT from MCSAT. We implicitly derive UNSAT if Resolution produces the empty clause and SAT if no new clauses can be derived (with Resolution or (Regular) Theory Derivation), thus essentially when a fixed point is reached. Note that this proof system does not (directly) allow to extract a satisfying assignment.
We now state and afterwards prove our core theorem.
Theorem 1. The Res * (T) proof system and the MCSAT proof system are equivalent with respect to their proof complexity on first-order logic with any theory.
T-Propagate: We give our proof in two steps: first we show that MCSAT can simulate Res * (T) -meaning that for any Res * (T) proof MCSAT can construct a proof that is at most polynomially longer -and finally show the reverse statement, that Res * (T) can simulate MCSAT. What we show is actually a slightly stronger statement: instead of constructing some proof (that is at most polynomially longer) we construct a logically equivalent proof, yielding something we could describe as algorithmic equivalency. Of course these proofs will not be syntactically identical, but they describe logically equivalent proof steps.
To show that MCSAT can simulate Res * (T), we need to show that MCSAT can simulate both the Resolution rule and the Strong Theory Derivation rule with at most polynomial overhead.
Assuming that our set of clauses C contains the clauses (C ∨ L) and (D ∨ ¬L), we need to add (C ∨ D) to C. Let us first handle a special case. Assume that we have a literal in C whose negation is in D. In this case (C ∨ D) ≡ true and there is nothing to do. Similarly, if (C ∨ D) ∈ C then we do not need to add it. From here on we assume that (C ∨ D) ≡ true and (C ∨ D) ∈ C. Starting from an empty trail, the clause (C ∨ D) can be learned using the MCSAT proof rules as follows:
First we apply the Decide rule for all literals L 1 , . . . , L n of C and D. Note that we start with the empty trail, thus initially all literals are undefined and can therefore be decided. Note furthermore that we assumed a finite Basis set that contains all literals from all clauses in C.
M
Now, the trail evaluates both C and D to false and we use the Propagate rule with (C ∨ L) to propagate L.
Propagate:
Having value(L, M ) = true now, (D ∨ ¬L) is conflicting and we apply the Conflict rule.
We perform resolution using the Resolve rule to obtain (C ∨ D).
Resolve:
To add the conflict clause to the set of clauses C we use the Learn rule.
Learn:
We have achieved our goal of adding (C ∨ D) to C and return to the initial state with the Restart rule.
Restart:
We observe that this sequence of proof rules is polynomial in the size of the clause (C ∨D) -we need |C|+|D|+5 rule applications -and we return to the same initial state afterwards, except for the added clause (C ∨ D). Note that we did not use any theory reasoning in the MCSAT rule applications and thus pay no hidden costs (as we later discuss in section 4).
We need to create some arbitrary clause C which is valid in the theory, that is T |= C. Similar to the previous simulation, we assume that C ≡ true and C ∈ C as there is nothing to do in these cases.
Our main hurdle is that MCSAT does not allow for learning arbitrary clauses but only the current conflict clause. We therefore have to construct an (artificial) conflict that yields the desired clause. We assume that our finite basis Basis includes all literals that ever occur in the Res * (T) proof. We can construct and learn an arbitrary (valid) clause C using the MCSAT proof rules as follows:
Starting again from the empty trail, we use Decide repeatedly to add ¬L for every L ∈ C to the trail. Note that Decide allows to decide any literal from Basis, independent on whether they appear in the input formula.
We know that C is a valid clause (T |= C) but we have value(C, M ) = false due to the previous decisions. Thus M is infeasible and we can apply the T-Conflict rule with E = C. Recall that a trail is infeasible if it is inconsistent in the theory -which is the case here as
Now we can learn the desired clause C using the Learn rule.
Learn:
Finally we return to the initial state with the Restart rule.
Restart:
We observe that we need |C| + 3 proof rule applications to learn an arbitrary clause (that is neither true nor already present in C) and return to the initial state.
We have seen that the MCSAT framework assumes that it can decide the feasibility of the trail, though (depending on the theory) deciding (in)feasibility might be computationally hard or even undecidable. While theorists might simply assume an "oracle" we now examine how actual implementations deal with this. Practically relevant implementations of infeasible(M ) for non-linear real arithmetic are incomplete. The respective papers suggest to apply the T-Conflict rule only if infeasibility can be detected by checking the consistency of univariate constraints. One might even (reasonably) argue that this restriction is not a technical one, but is a fundamental idea in MCSAT that allows the theory exploration in the first place -a complete implementation of infeasible(M ) would essentially prevent the theory exploration from happening (like in our simulation). Simulating the Strong Theory Derivation rule with an incomplete implementation of infeasible(M ) is a bit technical but doable, however, we need to consider also the length of the resulting proof.
The basic idea of the theory exploration in MCSAT is to guess a partial theory assignment (via T-Decide) until its infeasibility can be detected, generalize the unsatisfying assignment to an unsatisfying region around it (via T-Conflict) and exclude it (via Learn) from the further search and backtrack the theory assignment. This usually happens multiple times for a certain variable until the whole space is excluded for this variable and we have to change the assignment of the previously assigned theory variable.
In the above scenario the trail is already unsatisfiable due to the Boolean assignments, and we eventually discover this fact after exploring a certain number of regions and come up with a reason for the conflict. Note that the number of rule applications needed in this case grows with the number of regions we need to exclude and the complexity of this process highly depends on the background theory. For the question of completeness we refer to [dMJ] while we observe that for non-linear arithmetic, considering the number of cells a cylindrical algebraic decomposition may have to consider, the number of regions may easily grow exponentially (e.g. in the number of theory variables).
This unfortunately conflicts with our hope to find a polynomial reduction. However, this was to be expected: a major aspect of MCSAT is that certain parts of the theory reasoning are moved into the core proof system. Thus we should not be surprised if our core proof system exhibits bad asymptotic behavior if we consider a hard theory, while the proof system we compare it to completely hides the theory reasoning from the complexity measure. Note that theory reasoning for non-linear arithmetic based on cylindrical algebraic decomposition, whether it is infeasible(M ) in MCSAT or the question whether T |= C in Res * (T) may incur a doubly exponential runtime cost. We discuss how these two theory questions relate in section 4.
We thus conclude that the presented reduction is polynomial for the MCSAT proof system, but may not be for an actual MCSAT implementation. The additional complexity is however not new but only becomes visible as the MCSAT proof system makes the theory reasoning explicit while Res * (T) does not.
We observe that MCSAT has three separate places where clauses can "exist", namely the set of clauses C, the trail M and the current conflict clause C. When simulating MCSAT with Res * (T), we make sure that the set of clauses that Res * (T) operates on always includes C, clauses from M and C.
Note that Res * (T) retains all clauses that it constructs as is not designed to forget clauses while MCSAT may drop clauses occasionally. We note that removing clauses can bring advantages in practice, but the number of additional clauses is linear in the number of rule applications -MCSAT needs at least one rule application to construct a clause in the first place -and the practical overhead of additional clauses -for example due to larger lookup tables -is polynomial.
To prove that Res * (T) simulates MCSAT, it suffices to show that all clauses that ever occur in the MCSAT derivation can also be constructed using the Res * (T) proof rules. In case of unsatisfiability Res * (T) deduces the empty clause immediately before the application of the Unsat rule in MCSAT while any other termination of the Res * (T) proof system indicates satisfiability. We assume that initially both proof systems start with the same set of input clauses. We identify the rules where the MCSAT Resolve.
The Resolve rule takes the two clauses C (the current conflict clause) and D (from the trail M ) and produces the resolvent with respect to some literal L. By construction we know that Res * (T) has both C and D available and can thus apply the Resolution rule to produce the same resolvent.
Both the T-Propagate rule and the T-Conflict rule construct a new clause E by calling the MCSAT explain method. This method produces "a valid theory lemma" (as specified in [dMJ]), thus we have T |= E and can obtain these clauses using the Strong Theory Derivation rule.
As we have simulated all MCSAT rules that can be used to construct new clauses, we can now take any MCSAT proof and convert it into a Res * (T) proof by using the presented simulations for the Resolve, T-Propagate and T-Conflict rule and removing all other proof steps.
We have shown that MCSAT and Res * (T) simulate each other and are thus equivalent (in terms of proof complexity), concluding our proof for theorem 1.
One can very well argue that the length of a proof (in terms of proof steps) is not a satisfactory measure to assess the computational complexity of performing this proof. We already see in the analysis above that we can make proof rules arbitrarily powerful so that we can essentially prove anything with a single step. We could as well devise a prove system that executes individual processor instructions and thus requires an insane amount of proof steps. To compare proof systems it is thus crucial that they operate on a similar level of abstraction as we assume every proof rule to take some fixed amount of time.
One such abstraction is that we assume that theory queries (whatever a theory query may be in detail) only require constant effort here: one proof step for Strong Theory Derivation in Res * (T) and one proof step for either T-Propagate or T-Conflict in MCSAT. One may very well be worried here, as we know that theory queries for some theories can be extremely expensive (even doubly exponential for non-linear arithmetic using cylindrical algebraic decomposition) while all the other rules are easy to compute. This leads to two issues that influence how meaningful the above analysis is: how often are these particular rules used and do these theory queries have comparable computational effort?
If we use theory queries (almost) equally often in both proof systems, we can relax our assumption that all proof rules take constant time. Instead we consider theory rules (Strong Theory Derivation, T-Propagate and T-Conflict) and non-theory rules. We claim that all non-theory rules can be applied quickly (low polynomial runtime) and it suffices to consider their overall number as we did above. If we can additionally show that the theory rules have comparable computational effort in the different proof systems, this implies that the overall effort is (complexity-wise) the same.
Recalling the above reductions, we see that both proof systems need the exact same amount of theory rules. What remains to analyze is the computational effort for each of these theory queries. When Res * (T) simulates MCSAT (as described above) it generates the same clauses that MCSAT generated: if we would have an implementation for Strong Theory Derivation that would do this (significantly) more efficiently than whatever MCSAT does in the explain and infeasible methods, we could take this method and use it in MCSAT as well. We have also seen that MCSAT can simulate the Strong Theory Derivation rule (with a single theory call to the infeasible method while explain is trivial as no theory assignments are present [dMJ]) and thus a more efficient infeasible method would directly allow us to improve upon the implementation of the Strong Theory Derivation rule. We can just assume that both proof systems may use the exact same techniques for the theory queries and thus their computational effort is the same.
From the perspective of the SMT community the comparison to Res * (T) is of course interesting, but the actual question is how MCSAT relates to CDCL(T). Though we did not answer this specifically, we can both infer and speculate now more substantively than before. We know from [RKG] that CDCL(T) (with strong theory derivation) is equivalent to Res * (T) in terms of proof complexity as well, hence transitively MCSAT and CDCL(T) are equivalent (in terms of proof complexity).
CDCL(T) is presented as an algorithm in [RKG], but [NOT06] also (equivalently) defines CDCL(T) as a proof system. Though we cannot claim equivalency (beyond the aspect of proof complexity) between CDCL(T) and Res * (T), we can very well do so between MCSAT and Res * (T) as argued above. We conjecture that most proof rules from CDCL(T) and MCSAT nicely align and the ideas from the reductions above should be a good start for the remaining proof rules. Thus we believe that this work might be a first step towards a proof that establishes equivalency between CDCL(T) and MCSAT.
Like for MCSAT the theory queries within CDCL(T) are much more specific than those from Res * (T) and thus we expect the issues discussed in section 4 to essentially vanish here as well. Though the theory queries pose different questions, we know from practical implementations that the algorithms to answer them are very similar.
We have recalled the definitions of MCSAT (from [dMJ]) and Res * (T) (from [RKG]) and shown that they are equivalent with respect to their proof complexity, and even equivalent in a stronger sense that we described as algorithmically equivalent. We have discussed that though the complexity of theory queries is unknown, the fact that we simulate every theory query individually allows us to assume that the required effort is the same in both proof systems: if one would be (significantly) faster, we assume that the presented simulation can be used in the other proof system as well with only polynomial overhead. Still a more thorough analysis would be important to conduct in the future.
Finally we have discussed the importance of the presented work for the actual goal, the comparison of MCSAT and CDCL(T). We have noted that we established equivalency (in terms of proof complexity) of MCSAT and CDCL(T) which gives rise to the hope that they are in fact equivalent in the sense that they can (almost) directly simulate each other using the ideas presented here. A corresponding proof is also left for future work.