Satis ability-modulo-theories (SMT ) solving is a technique to check the satis ability of logical formulas. In the context of SMT solving, recently a novel technique called the model-constructing satis ability calculus (MCSAT ) was introduced in [13, 9], with a nice embedding of the cylindrical algebraic decomposition method as a theory solving module for non-linear real arithmetic [7]. In this paper we report on our work in progress on the embedding of the virtual substitution method in the MCSAT framework.
Satis ability-modulo-theories (SMT ) solving [1, 11] is a technique for checking the satis ability of (usually quanti er-free) rst-order logic formulas, i.e., Boolean combinations of constraints from an underlying theory. Typically, SMT solvers have two main components: a DPLL-CDCL-style SAT solver [4, 3, 12], which is responsible for the satisfaction of the Boolean structure of the formula, and one or more theory solvers, which assure consistency in the underlying theory.
These two components work together as follows: First, a Boolean abstraction of the input formula is built by replacing each theory constraint in the quanti er-free input formula by a fresh Boolean proposition, which encodes the truth value of the given theory constraint. The SAT solver searches for a satisfying solution for this Boolean abstraction, mainly by deciding to try a certain value for a propositional variable, propagating this decision to detect implications, and resolving con icts (via Boolean resolution, learning and backtracking) if the current partial assignment is detected to violate the formula. During its search, the SAT solver consults the theory solver(s) from time to time to check whether the constraints, whose abstraction variables are true under the current (possibly partial) Boolean assignment, together with the negation of those constraints whose abstraction variables are set to false1 are consistent.
If the SAT solver nds a complete Boolean solution for which the theory solver reports consistency then a solution for the input problem is found. If the 1 Under some mild conditions, only the constraints for the true abstraction variables need to be considered.
SAT solver nds no further solutions for the Boolean abstraction then the input problem is unsatis able. Otherwise, if the theory solver reports inconsistency for a (possibly partial) Boolean solution then it generates a theory lemma that explains the inconsistency. Learning the Boolean abstraction of this lemma (i.e., building the conjunction of the previous Boolean abstraction with the Boolean abstraction of the lemma) re nes the abstraction and should exclude at least the current (theory-con icting) Boolean assignment from the further search. The search continues until either satis ability on unsatis ability is detected.
When solving quanti er-free non-linear real arithmetic formulas, the theory solver(s) need to implement a decision procedure for checking the consistency (satis ability) of conjunctions of polynomial equalities and inequalities over the real domain. Besides the complete cylindrical algebraic decomposition (CAD ) method [2], also some incomplete algorithms like interval constraint propagation [5, 6] or the virtual substitution (VS ) method [14] can be adapted for this purpose.
Recently, a novel technique called the model-constructing satis ability calculus (MCSAT ) was introduced in [13, 9]. The main di erence to the previously described SMT framework is that MCSAT integrates the search for a theory model into the CDCL-style solving process. The MCSAT solving engine not only generates an assignment to satisfy the Boolean abstraction, but also produces values for the theory variables that are consistent with the current Boolean assignment. The future Boolean search is then directed by the theory assignment. Intuitively, consistent means in this context that the Boolean assignment of an abstraction variable and the evaluation of the corresponding constraint under the theory assignment never disagree; directed means that a Boolean decision will only be made if the corresponding constraint is still satis able under the current theory assignment.
If the solver wants to extend the current theory assignment by assigning a value to a theory variable x, it may be the case that there exists no such extension that would be consistent with the current Boolean assignment in the above sense. Then a theory solver is invoked with the current partial theory assignment and a conjunction (set) of theory constraints. These constraints do not need to be a priori con icting, but if we substitute the current partial theory assignment then they become univariate in x and have no common solution. The theory solver produces an explanation (in form of a theory lemma) why the current partial theory assignment cannot be extended to a solution that satis es all of its input constraints. This essentially corresponds to the role of theory lemmas in a regular SMT setting.
Di erent arithmetic decision procedures have been embedded as theory solving modules in the MCSAT framework, like the Fourier-Motzkin variable elimination procedure for quanti er-free linear real arithmetic [13], the CAD method for quanti er-free non-linear real arithmetic [7], the CAD method in combination with the branch-and-bound approach for quanti er-free non-linear integer arithmetic [8], and a mixed arithmetic and bit-blasting procedure for xed-size bit-vector arithmetic [15].
In the following we restrict ourselves to the theory of quanti er-free nonlinear real arithmetic. The goal of our work is to understand how the virtual substitution method can be e ciently embedded in the MCSAT framework. In the next section we explain the virtual substitution method at a high level. In Section 3 we describe our work-in-progress on the embedding of the virtual substitution method in MCSAT. In Section 4 we discuss future work. 2 2.1
Real Arithmetic and the Virtual Substitution Method
Given a nite set V = fx1; : : : ; xng of variables and a coe cient ring R, a polynomial p 2 R[x1; : : : ; xn] is an expression of the form p = Pid=1 ai jn=1xjeij with ai 2 R and ei;j 2 N0 for all i = 1; : : : ; d and j = 1; : : : ; n. The expressions ai jn=1xjeij are called terms, in which jn=1xjeij is a monomial and ai its coe cient. If n = 1 then we call p univariate, otherwise multivariate.
A multivariate polynomial p 2 R[x1; : : : ; xn] in variables x1; : : : ; xn and coefcients from R can also be seen as a univariate polynomial p 2 R[x1; : : : ; xn 1][xn] in the main variable xn having polynomial coe cients from the polynomial ring R[x1; : : : ; xn 1].
The degree of a monomial jn=1xjeij is the sum Pjn=i ei;j of the variables' exponents. The degree of a term is the degree of its monomial. The degree deg (p) of a polynomial p is the highest degree of its terms.
A polynomial constraint p 0 compares a polynomial to zero by an operator 2 f=; <; >; ; ; 6=g. A quanti er-free non-linear real arithmetic formula is a Boolean combination (using conjunction and negation) of polynomial constraints. 2.2
The virtual substitution (VS ) method is a quanti er elimination method for non-linear real arithmetic. In its original form, VS uses solution equations and therefore its applicability is restricted in the degree of the polynomials; novel developments allow, however, to extend the method to arbitrary degrees [10]. In this work we consider its application to the elimination of variables that appear at most quadratically in the input constraints as described in [14]. Furthermore, as we consider VS in the SMT solving context, we assume that the input formula for the VS method is a conjunction of polynomial constraints.
For a set of input polynomial constraints with polynomials from Z[x1; : : : ; xn] in which xn appears at most quadratically, the basic idea is to interpret the polynomials to be univariate in xn with polynomial coe cients (i.e., as polynomials from Z[x1; : : : ; xn 1][xn]) and to use the solution equation for quadratic polynomials to determine their zeros (see the top of Fig. 1).
If we would assign xed values to the coe cient variables x1; : : : ; xn 1 then all coe cients would evaluate to real values, and each input polynomial would case constant linear 1 0 = quadratic 1;2 = c b zeros
side condition
a = b = 0
a = 0 ^ b 6= 0
b p2ba2 4ac a 6= 0 ^ b2 4ac
case
p = 0, p 0, p 0
p 6= 0, p < 0, p > 0
be (
However, as the coe cients are polynomials, the degree of the polynomials, their zeros and the order of their zeros cannot be determined explicitly. Therefore, the VS method handles them symbolically : For each input constraint p 0, and for the cases where p is constant, linear or quadratic it speci es all possible real zeros of p along with side conditions for their existence (see the middle of Fig. 1).
Still, this symbolic description does not x the values of the zeros, nor their order. The VS method makes an elegant trick to overcome this problem: as a test candidate it takes the smallest point from each of the above-de ned regions. To do so, it allows to use the additional expressions 1 and + to express test candidates symbolically, where 1 stands for a value smaller than all zeros of all considered polynomials (in xn), is a (symbolic description of a) zero of one of the input polynomials, and + represents a value larger than but smaller than the next largest zero of any of the polynomials.
For each of the input constraints, the symbolic description gives us 7 possible
test candidates that cover all possible sign-invariant regions for all possible
evaluations of the coe cients: (
However, VS does not need to consider all these test candidates, as for each constraint p 0 the test candidates generated for p must satisfy p 0. This implies that for strict inequalities p 6= 0, p < 0 and p > 0 we do not need to consider the zeros of p. Furthermore, for non-strict inequalities it is su cient to consider 1 and the zeros of p only and the terms containing can be neglected. For further explanations we refer to [14].
Example 1. Assume that the VS gets two input constraints2 (x 2)2 + (y 2)2 1 < 0 and x y = 0. The varieties (zeros) of the polynomials are depicted in Fig. 2. We compute the following test candidates for the elimination of y: { 1 with side condition true, { 0 = x with side condition true for x y = 0, { 1 + with 1 = 2 p x2 + 4x 3 and side condition sc1 = ( x2 + 4x 0) for (x 2)2 + (y 2)2 1 < 0, and { 2 + with 2 = 2 + p x2 + 4x 3 and side condition sc2 = ( x2 + 4x 0) for (x 2)2 + (y 2)2 1 < 0. 3 3 tu
Assume that for a set of input constraints in the y variables x1; : : : ; xn (at most quadratic in xn) the VS method generates a set of test candidates for xn. Now, the set of input constraints is satis able if and only if there exists a test candidate for xn such that if we substitute this test candidate into the constraints than the resulting constraint system x is satis able. However, there is a last obstacle that needs to be overcome: the test candidates contain the expressions 1 and , and they might contain Fig. 2. The varieties of the square roots and polynomial fractions. Thus substi- polynomials (x 2)2 + (y tuting the test candidates directly will yield non- 2)2 1 and x y. arithmetic formulas. Therefore, the virtual substitution de nes substitution rules that yield satis ability-equivalent arithmetic expressions. We do not describe the virtual substitution rules here, but give some examples and refer to [14] for further reading.
Example 2. Virtually substituting the test candidates from Example 1 into the formula (x 2)2 + (y 2)2 1 < 0 ^ x y = 0 yields: { Substituting 1 for y evaluates to false, because the quadratic term will evaluate to +1 which is not negative. 2 Our computations do not demonstrate the full power of the VS method, as the equation x y = 0 could be used to eliminate x without considering test candidates for the quadratic equation. However, here we show the full computations to illustrate the basic mechanisms of the VS method.
1 false
1 < 0 ^ x y = 0 test candidates for y virtually substituting test candidates for y virtually substituting text candidates for x false 2(x 2)2
1 < 0 test candidates for x F1ig=. 32. Thpe VxS2 s+ea4rxch tree for the inputx(2x+ 42x)2 +3,(ysc1 2=)2sc21=<(0x2^ x 10 = 2 p2=2, and 20 =3,2 +2 p=2=22+. p y = 0 with 4x + 3 < 0), { Substituting 0 = x for y evaluates to 2(x 2)2 1 < 0 (by standard substitution). { Substituting 1 + with 1 = 2 p x2 + 4x 3 and side condition x2 + 4x 3 0 for y evaluates to false, because no equality can be satis ed by any value involving an in nitesimal.
Thus the virtual substitution method generates a search tree: having the input formula ' as root and a variable x1 (appearing at most quadratically) to be eliminated rst, a child node is generated for each test candidate for x1. The child node for a given test candidate t with side condition sc contains the formula '0 ^ sc after the application of the virtual substitution of t for x1.
This variable elimination procedure is repeated for all nodes containing nontrivial (true or false) formulas. The input formula is satis able if at least one of the leafs contains the formula true.
Example 3. The search tree generated by the virtual substitution for our running example (input constraints (x 2)2 + (y 2)2 1 < 0 ^ x y = 0) is shown in Fig. 3.
1 false 10+" true 0 = x 20+" false tu
Embedding the Virtual Substitution Method in the MCSAT Framework Basically, any quanti er elimination procedure can y be embedded as a theory solving module in MC- x SAT. Assume for simplicity a conjunction ' of the- x ory constraints. Assume furthermore an assignment y : fx1; : : : ; xng ! R that assigns some real values x to the variables x1; : : : ; xn such that does not evalu- Fig. 4. Illustration for ate ' to false, and such that each extension of with Example 4. an additional value assignment to a variable y evaluates ' to false. Then we can apply quanti er elimination to eliminate y in ', and use the resulting formula as an explanation for non-extensibility. y Example 4. Assume ' x y ^ y x, and let assign the value 1 to x. At this point there is no value for y with which we could extend the theory assignment such that ' is satis ed (see Fig. 4).
If we use the Fourier-Motzkin variable elimination procedure as a theory solving module to explain the con ict, we could eliminate y in x y ^ y x, which gives us the explanation (x y ^ y x) ! x 0. tu
However, the explanation we get this way might be stronger than we aim for: it might not only explain why the current theory assignment cannot be extended to y, but in general it rather gives the weakest precondition for the extensibility of any partial assignment with a value for y under the satisfaction of '.
At the rst sight it might seem optimal to derive and learn such weakest preconditions, rather than an explanation for the non-extensibility of the current theory assignment. However, some theory assignments might already be excluded for other reasons (e.g. by previously learnt lemmas). Though in theory it makes no di erence, for practical applicability we might want to reduce the size and/or the expressivity of the explanations to reduce the e ort for the further search.
Our idea for generating more precise explanations by the VS is based on the computation of a partial VS tree T ('; ; y) as follows. 1. We rst eliminate by VS the variable y from the input formula ' for which the partial theory assignment could not be extended. This results in a set of child formulas '1; : : : ; 'I . 2. For i = 1; : : : ; I, we do the following.
(a) Let m := 0 and 'i;0 = 'i. (b) If 'i;m has no variables (in which case 'i;m is false), continue with the next formula (i.e., increase i) starting at (2a). (c) Otherwise, we select the largest variable xi appearing in 'i;m according to the same variable order in which the partial theory assignment was extended. (d) We generate the list t1; : : : ; tl containing 1, and for all zeros of polynomials in 'i;m both as well as + . Let sc1; : : : ; scl be the corresponding side conditions.
1 false
1 false
1 < 0
test candidates for y
virtually substituting text candidates for x
Fpigx.52.+I4llxustr3a,tisocn1 f=or sEc2xa=mpl(ex25 w4ixth+ 31 <= 02), 10p= x22 + 4px2=2
20 = 2 + p2=2 2:70.
3, 2 = 2 +
1:29, and
(e) Remove those elements from the list whose side condition evaluates to
false under .
(f) We evaluate each of the remaining elements t from the list under
to constants (t), and determine an element L('i;m; ; xi) = t with
(t ) (xi) and for all other list elements t either (t) (t ) or
(xi) < (t); this element is a representative for the current xi-value
(xi) along the considered path.
(g) If t is a test candidate according to the VS rules then we virtually
substitute this test candidate t in 'i;m, which results in a new child
formula 'i;m+1. We increase m by 1 and continue at (2b).
(h) Otherwise, if t is not a test candidate according to the VS rules then
we stop the elimination for this path. We continue at (
This way we want to get a VS path from the root over each of the formulas '1; : : : ; 'I to a leaf. If we could now symbolically describe each of these paths, then we could generate an explanation stating that if ' holds then none of these path descriptions can be true.
Example 5. This example is illustrated in Fig. 5. Assume a formula ' = ((x 2)2 + (y 2)2 1 < 0) and a partial theory assignment with (x) = 0:5. This assignment cannot be extended to y, the reason being that the constraint ((x 2)2 + (y 2)2 1 < 0)[0:5=x] (y 2)2 + 1:25 < 0 is unsatis able.
We use the virtual substitution method to eliminate y from (x 2)2+(y 2)2 1 < 0, which results in three child formulas '1 = (false), '2 = (x2 4x + 3 < 0) and '3 = (false). At this point we could already return the explanation ' ! ('1 _ '2 _ '3), i.e., (x 2)2 + (y 2)2 1 < 0 ! x2 4x + 3 < 0, for the theory con ict.
But we could also continue the VS computations along the path that corresponds to the currently selected value (x) = 0:5. For the only non-false child node '2 = (x2 4x + 3 < 0) we get L('2; ; x) = 1. We virtually substitute this test candidate in '2, resulting in the formula false. Based on this VS computation we could learn the explanation (x 2)2 + (y 2)2 1 < 0 ! :(x < 1). tu
Next we explain how we can give a general symbolic description D of a path from a non-root node 'i;0 = 'i of our partial VS tree over the nodes 'i;1; : : : ; 'i;m 1 to a leaf 'i;m, based on a partial assignment to the variables of 'i such that cannot be extended to satisfy '.
Each such path represents a set of satis ability-equivalent assignments, but these assignment sets are not cylindrically arranged like it is the case for the cells of the CAD method. This means that there might be two di erent assignments, represented by the same path, which induce di erent orders over the test candidates for the variables. Though for each assignment we can uniquely identify the path (up to formula equality) that represents the current theory assignment, the symbolic description of a path is not quite straightforward.
We de ne the path description D('i;0; : : : ; 'i;M ) to be D('i;0) = 'i for
M M = 0 and ^m=1 ('i;m 1; 'i;m) otherwise. For the basic part, we propose three di erent de nitions for ('i;m 1; 'i;m), which we distinguish as 1, 2 and 3; similarly, we will write D1, D2 resp. D3 when using 1, 2 resp. 3. Note that 'i;m is a child node of 'i;m 1. Assume that in the node 'i;m 1 the VS method generated test candidates for a variable xi. We consider all (symbolic) zeros Ttrue = ft1; : : : ; tl; t01; : : : ; t0ug of all polynomials in 'i;m 1 whose side conditions are true under , and assume for them w.l.o.g. the order (t1) 1 (t2)
2 : : : l 1 (tl) l (xi) < (t01) 01 : : : 0u 1 (t0u) under the current partial theory assignment with k; 0k2 f<; =g for all k. If l = 0 then there is no test candidate below (xi); similarly, u = 0 represents the case where there is no test candidate larger than (xi). Let analogously Tfalse be the set of all (symbolic) zeros of all polynomials in 'i;m 1 whose side conditions are false under .
1('i;m 1; 'i;m) 8> sc(tl) ^ xi = tl if l > 0 and l is = >>>>>> Vt2Ttrue sc(t) ^ Vt2Tfalse :sc(t)^ >>>>>>>> tl < xi ^ xi < t01 ^ (Vlk=11 tk k tkif+l1)>^0(,Vuku=>110t0kand0k t0kl+i1s) < > = < Vt2Ttrue sc(t) ^ Vt2Tfalse :sc(t) ^ tl < xi ^ (Vlk=11 tk k tk+1) >>>> if l > 0, u = 0 and l is < >>>>> Vt2Ttrue sc(t) ^ Vt2Tfalse :sc(t) ^ xi < t01 ^ (Vku=11 t0k k t0k+1) >>>>> if l = 0 and u > 0 >:> Vt2Tfalse :sc(t) else (if l = 0 and u = 0) 2('i;m 1; 'i;m) >8 sc(tl) ^ xi = tl if l > 0 and l is = > >>>> sc(tl) ^ sc(t01) ^ tl < xi ^ xi < t01 ^ Vt2Tfalse[Ttrue sc(t) ! (t tl _ t01 t) > >>>> if l > 0, u > 0 and l is < = < sc(tl) ^ tl < xi ^ Vt2Tfalse[Ttrue sc(t) ! t tl >>>> if l > 0, u = 0 and l is < > >>>> sc(t01) ^ xi < t01 ^ Vt2Tfalse[Ttrue sc(t) ! t01 t if l = 0 and u > 0 >:> Vt2Tfalse :sc(t) else (if l = 0 and u = 0) 3('i;m 1; 'i;m) > >>>: Vt2Tfalse[Ttrue sc(t) ! (xi < t) 8> sc(tl) ^ xi = tl if l > 0 and l is = > = >>< sc(tl) ^ tl < xi ^ Vt2Tfalse[Ttrue sc(t) ! (t tl _ xi < t) if l > 0 and l is < else (if l = 0) The formula 1 provides the most strict description of why the current theory assignment is not extensible, whereas 2 and 3 o er a more general explanation. More formally, (9xi: 'i;m 1 ^ 1('i;m 1; 'i;m)) ! 'i;m (9xi: 'i;m 1 ^ 2('i;m 1; 'i;m)) ! 'i;m (9xi: 'i;m 1 ^ 3('i;m 1; 'i;m)) $ 'i;m and by the de nition of D1, D2 and D3 we get (9x1; : : : ; xi: 'i;0 ^ D1('i;0; : : : ; 'i;m)) ! 'i;m (9x1; : : : ; xi: 'i;0 ^ D2('i;0; : : : ; 'i;m)) ! 'i;m (9x1; : : : ; xi: 'i;0 ^ D3('i;0; : : : ; 'i;m)) $ 'i;m Finally, let = f 1; : : : ; kg be all paths (as formula sequences) in the partial VS tree T ('; ; y) from the I children of the root node to the leaves 'i;mi (note that all generated leafs are false and that there are exactly I leaf nodes). Then
I ' ! ( _ :D( i) _ 'i;mi )
i=1 is a tautology for D 2 fD1; D2; D3g.
As a last remark, perhaps the reader has recognised that we explicitly referred to zeros of polynomials in the above descriptions. Instead of explicit references, in the implementation we will use a special syntax zero(i; p) as in [7] to refer to the ith zero of a polynomial p. 4
Future Work The work described in this progress report is ongoing. We do believe that the presented statements are true, but of course the presented ideas need to be formalised more precisely, and proofs for the statements need to be given. After this step, we will develop a pseudo-algorithmic description of the explanation generation for the VS method in the MCSAT context, and implement the approach based on our SMT solver SMT-RAT. Currently we work on the implementation of the CAD embedding in MCSAT. Once that implementation is nished, we can reuse modules (like the SAT module extended with theory decision and propagation) for the embedding of the VS method. The implementation of the MCSAT-embedding of the virtual substitution will allow us to compare the different explanation generation mechanisms discussed in this paper, and thus to collect experiences which ideas are the most promising from the perspective of (time and memory) e ciency.
Though the MCSAT embedding of the CAD method in the Z3 SMT solver has been shown to be very e cient, we believe that harder arithmetic problems can be solved most e ciently by combinations of di erent decision procedures. To do so, we will use the possibilities o ered by SMT-RAT for the strategic combinations of theory solving modules: for quadratic problems we will employ the VS and for (sub-)problems beyond the capabilities of our VS module we will use the CAD method in the context of the MCSAT framework. 5. Gao, S., Ganai, M., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems.
In: Proc. of FMCAD'10. pp. 81{90. IEEE (2010) 6. Herbort, S., Ratz, D.: Improving the e ciency of a nonlinear-system-solver using a componentwise Newton method. Tech. Rep. 2/1997, Inst. fur Angewandte Mathematik, University of Karlsruhe (1997) 7. Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Proc. of IJCAR'12.
LNAI, vol. 7364, pp. 339{354. Springer (2012) 8. Jovanovic, D.: Solving nonlinear integer arithmetic with MCSAT. In: Proc. of VM
CAI'17. LNCS, vol. 10145, pp. 330{346. Springer (2017) 9. Jovanovic, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satis ability calculus. In: Proc. of FMCAD'13 (2013) 10. Kosta, M.: New Concepts for Real Quanti er Elimination by Virtual Substitution.
Ph.D. thesis, Saarland University (2016) 11. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View.
Springer (2008) 12. Marques-silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satis ability. IEEE Transactions on Computers 48, 506{521 (1999) 13. de Moura, L., Jovanovic, D.: A model-constructing satis ability calculus. In: Proc.
of VMCAI'13. pp. 1{12. Springer (2013)
14. Weispfenning, V.: Quanti er elimination for real algebra - the quadratic case and
beyond. Appl. Algebra Eng. Commun. Comput. 8(