Satis ability-modulo-theories (SMT ) solving is a technique for checking the satis ability of logical formulas. In this context, recently a framework called model-constructing satis ability calculus (MCSAT ) has been introduced which relaxes some design restrictions of the classical SMT setting and allows more freedom to construct an e cient interplay between the search for models in the Boolean and the theory domains. In this paper we discuss issues of dynamic variable orderings to drive the MCSAT model search for the theory of non-linear real arithmetic.
until either both the SAT and theory solver have constructed a complete assignment for both the Boolean and theory variables or all Boolean assignments have been excluded.
Recently, a framework called model-constructing satis ability calculus (MCSAT ) was introduced [JdM12, dMJ13], which allows the simultaneous construction of Boolean and theory models, enabling more freedom for the design of the interplay between the search in the Boolean and in the theory domains. In this approach, the Boolean and theory modules from the classical framework are merged into a single solver that works on the Boolean structure and the theory simultaneously. This solver performs decisions not only on the Boolean (abstraction) variables, but also on the theory variables by making theory decisions. Throughout the procedure, the two models are kept consistent, meaning that the truth values of constraints at the Boolean level never contradict to their evaluation under the theory model. When the current partial theory model cannot be further extended to a complete and consistent theory model, theory con ict resolution is applied to generate an explanation in form of a lemma that can be learned to exclude this and \similar" inconsistent guesses from the further search.
In quanti er-free non-linear real arithmetic, the constraints are polynomial equalities or inequalities over the real domain. For this theory, we have implemented in our SMT-RAT solver [CKJ+15] di erent theory solver modules for classical SMT solving. Additionally, we have also adapted for MCSAT the cylindrical algebraic decomposition method (CAD ), the virtual substitution method (VS ) and the Fourier-Motzkin variable elimination method (FM ) for generating explanations. For CAD, we employ the approach outlined in [JdM12] (commonly known as nlsat), where we support di erent projection operators, and alternatively implement an adaptation of the OneCell-CAD approach presented in [Bro13, BK15] for explanation generation as described in [Neu18]. The adaptation of VS is based on our presentation from [ANK17], where elimination is restricted to the unassigned variables. The Fourier-Motzkin variable elimination is adapted in the spirit of [JBdM13], enhanced with explicit support for equalities and weak inequalities.
It is well-known that the variable ordering is a crucial ingredient both in theory and practice for many solving techniques. For all of the above methods { SAT solving, FM, VS and CAD { the variable ordering can move the performance from the worst-case to \almost trivial" or vice-versa. At the same time nding the best (or at least a \good") variable ordering in a reasonable amount of time is essentially impossible in all cases. Thus heuristics are heavily used in practice to nd reasonably good variables orderings quickly.
The original MCSAT approach for non-linear real arithmetic [JdM12] assumes a static ordering of theory variables. This static variable ordering guides also the Boolean search: the solver identi es those clauses that are univariate in the rst unassigned variable in the static theory variable ordering under the current theory model (i.e., the rst unassigned theory variable is the only unassigned one occurring in them) and performs Boolean propagations and Boolean decisions only with respect to those clauses. If all such clauses are satis ed at the Boolean level then the next theory decision is made, extending the theory model in agreement with the Boolean model (if possible). While we can use a form of con ict-driven activity-based heuristics (like VSIDS) for the Boolean variables, the static theory variable ordering heavily restricts the exibility here.
The restriction to consider univariate clauses only was already lifted in [dMJ13] and the possibility to even include the theory variables in such an activity-based heuristic { essentially treat Boolean and theory variables equally in one combined variable ordering { was proposed [JBdM13]. Note however that [dMJ13] described the general MCSAT framework independently of a speci c theory and [JBdM13] only discusses linear real arithmetic (combined with uninterpreted functions). Unfortunately, this does not directly transfer to non-linear real arithmetic: while regular polynomial constraints have a clear semantic meaning independently of the variable ordering, we need to consider extended polynomial constraints (as de ned in [JdM12]) that pose additional challenges under changing variable orders.
In the remainder of this paper we discuss how to design MCSAT for non-linear real arithmetic with dynamic theory variable ordering, meaning that the ordering of any variables may change throughout the computation. This includes necessary algorithmic modi cations, some considerations for the implementation and completeness issues. Finally, we report on some preliminary experiments. We assume the reader to be reasonably familiar with the MCSAT framework as presented in [JdM12, dMJ13] as well as SAT solving and classical SMT solving. 2
The fundamental idea of MCSAT is to construct the Boolean model and theory model simultaneously. This allows the Boolean reasoning and the theory reasoning to complement (and possibly learn from) each other more exibly than in traditional SMT solving. The variable scheduler is the crucial component driving this process, mainly determining how we interleave Boolean and theory reasoning. Given the importance of the variable ordering on practical performance, it is possible (even probable) that more elaborate computations in the scheduling heuristics pay o in terms of overall solving time.
When devising a variable scheduling heuristic we need to answer two questions: Firstly, how should we interleave (or prioritize) the Boolean and theory reasoning? Secondly, how should the variables (both Boolean and theory) be ordered? For Boolean variables solvers usually rely on con ict-driven activity-based heuristics like VSIDS while theory variables are mostly static (based on some heuristic) throughout the whole solving process.
Experience shows that constructing a good variable ordering upfront is hard. Even for a pure CAD (or VS) computation that is not embedded in some other framework (like traditional SMT or MCSAT) the results are mixed. The existing heuristics almost exclusively focus on syntactic properties (like variable degree or number of occurrences), and adversarial inputs seem to be neither hard to construct nor particularly contrived or arti cial.
Similar to CDCL-style SAT solving { and following [JBdM13] { we therefore use a dynamic variable ordering for theory variables as well in the hope to learn an e cient variable ordering during solving. 2.1
Our implementation contains several changes compared to the descriptions from [JdM12, dMJ13, JBdM13] that in uence which heuristics can be used and how we can implement them. Some are clearly beyond the previously published descriptions while others are possibly intended by the authors but have not been made explicit.
Our core solver is based on a CDCL-style SAT solver (MiniSAT) and thus incorporates all common optimizations and heuristics that go beyond what is presented in [JdM12, dMJ13] for the Boolean reasoning. A set of active literals is maintained that contains those literals occurring in not-yet satis ed clauses. It is su cient to decide only literals from this set to obtain a complete procedure.
Before a Boolean decision is made, we check for feasibility together with the current theory model. That is, after deciding the constraint we do not run into an immediate theory con ict. If the constraint is not feasible, we insert its negation as a lazy theory propagation. If this propagation leads to a con ict later on, the explanation is generated on request. This is essentially one concrete way how to apply the T-Propagate rule from [dMJ13].
Whenever a theory assignment is computed, we optionally apply substitution of the current partial model in the assigned literals, collect those that are linear after the substitution and use a Simplex-based solver to check their consistency. This may yield a satisfying model for the whole set of assigned literals, or allow to determine infeasibility earlier.
We combine multiple explanation backends (similar to [JBdM13]) based on FM, VS, CAD as in [JdM12] and OneCell-CAD. Besides allowing to fall back to \more complete" explanation backends, the variable scheduler could also exploit a particular combination of backends by favouring constraints that can be handled by more e cient methods (for example linear constraints). 2.2
To evaluate the implementation and get a rst feeling on the impact in practice, we consider several di erent variable orderings here: Boolean rst. All Boolean variables are decided rst with an activity-based dynamic ordering before any theory decision is made. We use a static theory variable ordering based on features like maximum degrees or coe cients roughly following the \triangular ordering" from [EBDW14]. Many possibilities here are yet unexplored, for example other variable orderings proposed in [EBDW14] or [DSS04].
Theory rst. Same as Boolean rst, but theory decisions are made before any Boolean decision is made. Note that after deciding all theory variables, only Boolean variables not representing a theory constraint need to be decided.
Univariate constraints. Like before we use a static ordering for theory variables and a dynamic ordering for Boolean variables. For Boolean decisions we only consider variables that are univariate under the current theory model and perform a theory decision if none is left. This interleaves the Boolean and theory reasoning and, combined with active literals tracking, is very similar to nlsat from [JdM12].
Uniform activies. As in [JBdM13], the activity is tracked for both Boolean and theory variables in a con ictdriven manner (like VSIDS). For Boolean variables, those are the resolution variables, and for theory variables, those are the ones occurring in the corresponding theory constraints, counted only once per con ict.
The unassigned variable (Boolean or theory) with highest activity is decided rst.
Random. A random ordering over all variables (Boolean and theory) is xed and decided in this order. This strategy is only used as a reference. 3
As already noted using a dynamic ordering for theory variables has some consequences that go well beyond what we know from regular SMT solving. 3.1
Explanations from a CAD-based explanation backend may contain extended polynomial constraints of the form y
rooti(p(z; x1; : : : ; xn)) where 2 f<; >; =; 6=; ; g, y; z; x1; : : : ; xn are real-valued variables, p is a polynomial with rational coe cients and variables z; x1; : : : ; xn. If x1; : : : ; xn are assigned to values (x1); : : : ; (xn), then rooti(p(z; x1; : : : ; xn)) represents the ith zero of the univariate polynomial p(z; (x1); : : : ; (xn)) in z. Such a constraint evaluates to true if the ith root exists and (y) compares to this root as indicated by , and to false otherwise.
Assuming a xed theory variable ordering, the way how such extended polynomial constraints are constructed within the explanation guarantees that for each of these constraints x1; : : : ; xn are assigned before y and thus the above semantics are well-de ned. Changing the theory variable ordering may lead to a situation where y is assigned while some xi 2 fx1; : : : ; xng is still unassigned if the respective constraint was generated under a di erent variable ordering. In some sense, we no longer have a constraint on y but a constraint on xi. Since the semantics for such an expression is not well-de ned, a consistent value for xi cannot be calculated making theory decisions impossible. Note that the above semantics could be extended, but actually using constraints under these extended semantics has proven to be extremely di cult { if not impossible { in practice.
We currently employ a rather simple solution: we disable (i.e. exclude from theory consistency checks) all constraints of the form y rooti(p(z; x1; : : : ; xn)) where some x1; : : : ; xn is not yet assigned but y has been chosen for a decision. We observe that constraints are not necessarily disabled if the ordering changes but only if the ordering becomes incompatible (y moves before one of x1; : : : ; xn). Note that constraints can safely be re-enabled, whenever its ordering is compatible with the current one again: Then, they do not immediately evaluate to a value as at least y is not assigned.
Note that after disabling a constraint, the regions excluded by it might be considered again. However, this does endanger termination: For any region and for each particular ordering, at most nitely many explanations are generated excluding this region. Additionally, any two explanations excluding a common region but generated under di erent incompatible orderings either are unequal or one of them is not generated (as then, no constraint would have been disabled); thus, no explanation is learned twice. 3.2
While a SAT solving process advances with any Boolean con ict resolution, for MCSAT the explanation backends need to ful ll additional requirements for completeness. The completeness proof of MCSAT from [JdM12] requires that all constraints occurring in an explanation clause must come from some nite set of constraints that depends on the input formula; we then say that an explanation backend ful ls the nite basis property. This property holds for all the described explanation backends individually under a static theory variable ordering based on the following (inductive) argument: given a nite set of k-dimensional constraints, these explanation backends can construct only nitely many new constraints of dimension k 1 or less and we can (conceptually easily) enumerate all of them. Based on this enhanced set, we can construct the constraints of dimension k 2 or less, and so on, ultimately obtaining a nite basis.
This argument still holds if we combine multiple explanation backends using the same static variable ordering. Note that the variable ordering of these explanation backends is not identical by construction: while the ordering on the assigned variables is xed by the MCSAT trail we can have multiple unassigned variables whose ordering is unspeci ed. Though explanations never contain unassigned variables, it is not immediately clear whether explanation backends that use di erent orderings for unassigned variables can be combined safely.
If the variable ordering is dynamic, we lose the nite basis property as we can see from the counterexample for Fourier-Motzkin and VS shown in Example 1 and we assume similar examples to exist for CAD. Though this technically does not prove incompleteness, we doubt that some weaker property exists so that the procedure still terminates in all cases with an in nite basis for explanations.
Example 1 For the set of constraints fx1 = 2; x1 = 2x2; x2 = 2x1g | {c1z } | {c2z } | {c3z } an in nite sequence of new constraints can be created by either FM or VS steps: eliminating x1 in fc1; c2g gives c4 : x2 = 1, eliminating x2 in fc3; c4g gives c5 : 2x1 = 1, eliminating x1 in fc2; c5g gives c6 : 4x2 = 1, eliminating x2 in fc3; c6g gives c7 : 8x1 = 1, . . .
We can assure completeness with a stronger version of what we described as disabled constraints in Section 3.1: we store the variable ordering that was used when some clause was constructed and disable the whole clause for decisions and propagations when the current variable ordering is incompatible. With the same argument as given in Section 3.1, the procedure remains complete as lemmas are not generated twice and we only have nitely many variable orderings.
However, our main goal in making the theory variable ordering dynamic is not to work on the core problem from di erent perspectives { as one could understand CDCL-style SAT solving { but rather nd an advantageous ordering dynamically and eventually settle on this one. The (syntactic) nite basis property ensures that every con ict makes at least a certain amount of progress (by excluding one of nitely many regions). Ever-changing theory variable orderings can easily lead to non-termination in MCSAT as we have seen in Example 1 by (potentially) excluding in nitesimally small regions. Note however that we consider this a theoretical issue: if we ensure that the theory variable ordering becomes stable at some point, similar to how restarts are handled in CDCL-style SAT solving, we can assume this to be safe in practice. 4
The relative performance of the heuristics we de ned above on the SMT-LIB benchmark set for QF NRA are shown in Table 1 and Figure 1. It should be noted that a large part of the SMT-LIB [BFT16] benchmark set for QF NRA has no complex Boolean structure. Throughout the experiments, we used a combination of the FM, VS and Onecell-CAD explanation backends by calling them in this order and falling back to the next backend if one failed.
We observe that the Boolean rst strategy works only slightly better than a random ordering and signi cantly worse than most other heuristics. Univariate constraints improves upon this, in particular if combined with active literals tracking which is close to the nlsat heuristic from [JdM12]. However, active literals tracking
Random Boolean rst Univariate Univariate + active literals Uniform activities
Theory rst 0 8:8k 8:85k 8:9k 8:95k 9k 9:05k 9:1k 9:15k 9:2k 9:25k 9:3k 9:35k 9:4k 9:45k 9:5k
# solved problems brings no bene t when combined with Theory rst or Uniform activities. The Uniform activities and Theory rst strategies perform best with Theory rst having a slight advantage in terms of the average running time.
The success of both the Theory rst and Univariate + active literals strategies may indicate that the nlsat strategy from [JdM12] is e ective because Boolean decisions are delayed, and it actually delays them even more than the Univariate + active literals strategy: while we only consider univariate literals from not yet satis ed clauses, nlsat only considers literals from univariate clauses. We did not yet implement the nlsat strategy in our solver.
One may assume that the Uniform activities strategy performs well because it essentially converges towards the Theory rst ordering. This is however not the (only) reason for its e ectiveness. We experimented with ways to further increase the activities of theory variables compared to Boolean variables: increasing activities of theory variables multiple times per con ict; strictly favouring theory variables in the case of equal activities; using the Theory rst strategy where the theory variables are ordered according to activities. All of those performed worse than just using uniform activities, suggesting that Uniform activities and Theory rst are e ective for di erent reasons. 5
We have seen that the variable ordering has a signi cant impact on the overall performance and might be the key to better running times in practice. We only had a rst glimpse of the possibilities that result from dynamic variable orderings. It is not clear yet that lifting all restrictions are strictly bene cial, but the preliminary experiments we presented could be evidence for this.
We aim at investigating other variable ordering schemes that combine established dynamic heuristics from SAT solving with variable ordering heuristics borrowed from the computer algebra community. It should be noted however that experimenting with variable orderings should not be overly specialized by \over tting" to the SMT-LIB benchmark set.
Dynamic variable orderings also give rise to theoretical questions about the completeness of MCSAT. While we presented evidence for non-termination (under extremely pessimistic assumptions about MCSAT), we conjecture that termination can be assured for reasonable (dynamic) variable orderings with arguments resembling the use of restarts in SAT solving. [ANK17]