Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework (Work-in-progress Paper) Erika Ábrahám, Jasper Nalbach, and Gereon Kremer RWTH Aachen University, Germany Abstract. Satisfiability-modulo-theories (SMT ) solving is a technique to check the satisfiability of logical formulas. In the context of SMT solv- ing, recently a novel technique called the model-constructing satisfiability calculus (MCSAT ) was introduced in [13, 9], with a nice embedding of the cylindrical algebraic decomposition method as a theory solving mod- ule 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. 1 Problem Statement Satisfiability-modulo-theories (SMT ) solving [1, 11] is a technique for check- ing the satisfiability of (usually quantifier-free) first-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 the- ory. These two components work together as follows: First, a Boolean abstrac- tion of the input formula is built by replacing each theory constraint in the quantifier-free input formula by a fresh Boolean proposition, which encodes the truth value of the given theory constraint. The SAT solver searches for a satis- fying solution for this Boolean abstraction, mainly by deciding to try a certain value for a propositional variable, propagating this decision to detect implica- tions, and resolving conflicts (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 cur- rent (possibly partial) Boolean assignment, together with the negation of those constraints whose abstraction variables are set to false1 are consistent. If the SAT solver finds 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 finds no further solutions for the Boolean abstraction then the input problem is unsatisfiable. 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) refines the abstraction and should exclude at least the current (theory-conflicting) Boolean assignment from the further search. The search continues until either satisfiability on unsatisfiability is detected. When solving quantifier-free non-linear real arithmetic formulas, the theory solver(s) need to implement a decision procedure for checking the consistency (satisfiability) 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 satisfiability calcu- lus (MCSAT ) was introduced in [13, 9]. The main difference 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 as- signment. 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 satisfiable 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 conflicting, 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 satisfies all of its input constraints. This essentially corresponds to the role of theory lemmas in a regular SMT setting. Different arithmetic decision procedures have been embedded as theory solv- ing modules in the MCSAT framework, like the Fourier-Motzkin variable elimi- nation procedure for quantifier-free linear real arithmetic [13], the CAD method for quantifier-free non-linear real arithmetic [7], the CAD method in combina- tion with the branch-and-bound approach for quantifier-free non-linear integer arithmetic [8], and a mixed arithmetic and bit-blasting procedure for fixed-size bit-vector arithmetic [15]. In the following we restrict ourselves to the theory of quantifier-free non- linear real arithmetic. The goal of our work is to understand how the virtual substitution method can be efficiently 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 Real Arithmetic and the Virtual Substitution Method 2.1 Quantifier-free Non-linear Real Arithmetic Given a finite set V = {x1 , . . . , xn } of variables and a coefficient ring R, a poly- Pd n eij nomial p ∈ R[x1 , . . . , xn ] is an expression of the form p = i=1 ai Πj=1 xj with ai ∈ R and ei,j ∈ N0 for all i = 1, . . . , d and j = 1, . . . , n. The expres- n e n e sions ai Πj=1 xj ij are called terms, in which Πj=1 xj ij is a monomial and ai its coefficient. If n = 1 then we call p univariate, otherwise multivariate. A multivariate polynomial p ∈ R[x1 , . . . , xn ] in variables x1 , . . . , xn and coef- ficients from R can also be seen as a univariate polynomial p ∈ R[x1 , . . . , xn−1 ][xn ] in the main variable xn having polynomial coefficients from the polynomial ring R[x1 , . . . , xn−1 ]. n e Pn The degree of a monomial Πj=1 xj ij is the sum j=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 opera- tor ∼∈ {=, <, >, ≤, ≥, 6=}. A quantifier-free non-linear real arithmetic formula is a Boolean combination (using conjunction and negation) of polynomial con- straints. 2.2 The Virtual Substitution Method The virtual substitution (VS ) method is a quantifier 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 poly- nomials to be univariate in xn with polynomial coefficients (i.e., as polynomials from Z[x1 , . . . , xn−1 ][xn ]) and to use the solution equation for quadratic polyno- mials to determine their zeros (see the top of Fig. 1). If we would assign fixed values to the coefficient variables x1 , . . . , xn−1 then all coefficients would evaluate to real values, and each input polynomial would p∼0 p = ax2 + bx + c ∼∈ {=, <, >, ≤, ≥, 6=} case zeros side condition constant −∞ a=b=0 linear ξ0 = − cb √ a = 0 ∧ b 6= 0 −b± b2 −4ac quadratic ξ1,2 = 2a a 6= 0 ∧ b2 − 4ac ≥ 0 case test candidates (samples) p = 0, p ≤ 0, p ≥ 0 −∞ ξ0 ξ0 + ε ξ1 ξ1 + ε ξ2 ξ2 + ε p 6= 0, p < 0, p > 0 −∞ ξ0 ξ0 + ε ξ1 ξ1 + ε ξ2 ξ2 + ε Fig. 1. Test candidates (in black) generated by the VS for an input constraint p ∼ 0 be (1) either constant zero or constant non-zero, (2) or linear with exactly one real zero, (3) or quadratic with at most two real zeros. These zeros would divide the real domain for xn into a finite set of regions over which the signs of the polynomials do not change. These regions are given by the zeros themselves, the regions between two successive zeros, and the regions below the smallest zero and above the largest zero. Thus we could pick a test candidate from each of the regions and check whether one of them satisfies all input constraints. If it is the case them we have found a solution, otherwise the input constraints are inconsistent. However, as the coefficients are polynomials, the degree of the polynomials, their zeros and the order of their zeros cannot be determined explicitly. There- fore, the VS method handles them symbolically: For each input constraint p ∼ 0, and for the cases where p is constant, linear or quadratic it specifies 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 fix 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-defined regions. To do so, it allows to use the additional expressions −∞ and ξ +  to express test candidates symbolically, where −∞ 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 eval- uations of the coefficients: (1) for a constant polynomial, being sign-invariant over the whole real domain, we take −∞ as a representative, (2) for a linear polynomial, having exactly one zero ξ0 , the candidate −∞ represents the re- gion left of this zero, ξ0 the zero itself, and ξ0 +  the region to the right of it, and (3) for the quadratic case with at most two zeros ξ1 and ξ2 , under the assumption that their existence is assured by the corresponding side conditions, the candidates −∞, ξ1 , ξ1 + , ξ2 and ξ2 +  represent all sign-invariant regions, independently of the order of the zeros ξ1 and ξ2 (see bottom of Fig. 1). 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 sufficient to consider −∞ 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: – −∞ with side condition true, – ξ0 = x with side condition √ true for x − y = 0, – ξ1 +  with ξ1 = 2 − −x2 + 4x − 3 and side condition sc1 = (−x2 + 4x − 3 ≥ 0) for (x − 2)2 + (y √ − 2)2 − 1 < 0, and – ξ2 +  with ξ2 = 2 + −x2 + 4x − 3 and side condition sc2 = (−x2 + 4x − 3 ≥ 0) for (x − 2)2 + (y − 2)2 − 1 < 0. t u 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 satisfiable 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 satisfiable. However, there is a last obstacle that needs to be overcome: the test candidates contain the expressions −∞ and , and they might contain Fig. 2. The varieties of the square roots and polynomial fractions. Thus substi- polynomials (x − 2)2 + (y − 2 tuting the test candidates directly will yield non- 2) − 1 and x − y. arithmetic formulas. Therefore, the virtual substi- tution defines substitution rules that yield satisfiability-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 −∞ for y evaluates to false, because the quadratic term will evaluate to +∞ 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. (x − 2)2 + (y − 2)2 − 1 < 0 ∧ x − y = 0 test candidates for y ξ1 +ε ξ2 +ε −∞ ξ0 = x +side condition sc1 +side condition sc2 virtually substituting test candidates for y false false false 2(x − 2)2 − 1 < 0 test candidates for x −∞ ξ10 +ε ξ20 +ε virtually substituting text candidates for x false true false 2 2 Fig. 3. The √ (x − 2) + (y − 2) − 1 < 0 2∧ x − y = 0 with √ VS search tree for the input ξ1 = 2 −√ −x + 4x − 3, ξ2 √ 2 = 2 + −x + 4x − 3, sc1 = sc2 = (x − 4x + 3 < 0), 2 ξ10 = 2 − 2/2, and ξ20 = 2 + 2/2. – Substituting ξ0 = x for y evaluates to 2(x − 2)2 − 1 < 0 (by standard substitution). √ – Substituting ξ1 +  with ξ1 = 2 − −x2 + 4x − 3 and side condition −x2 + 4x − 3 ≥ 0 for y evaluates to false, because no equality can be satisfied by any value involving an infinitesimal. t u 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 first, 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 non- trivial (true or false) formulas. The input formula is satisfiable 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. t u 3 Embedding the Virtual Substitution Method in the MCSAT Framework y Basically, any quantifier elimination procedure can y x≤ be embedded as a theory solving module in MC- SAT. Assume for simplicity a conjunction ϕ of the- x ory constraints. Assume furthermore an assignment y≤ ν : {x1 , . . . , xn } → 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 quantifier elimination to eliminate y in ϕ, and use the resulting formula as an explanation for non-extensibility. 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 satisfied (see Fig. 4). If we use the Fourier-Motzkin variable elimination procedure as a theory solving module to explain the conflict, we could eliminate y in x ≤ y ∧ y ≤ −x, which gives us the explanation (x ≤ y ∧ y ≤ −x) → x ≤ 0. t u 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 first 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 difference, for practical applicability we might want to reduce the size and/or the expressivity of the explanations to reduce the effort 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 first 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 −∞, and for all zeros ξ of polynomials in ϕi,m both ξ as well as ξ + . Let sc1 , . . . , scl be the cor- responding side conditions. (x − 2)2 + (y − 2)2 − 1 < 0 test candidates for y ξ1 +ε ξ2 +ε −∞ +side condition sc1 +side condition sc2 virtually substituting test candidates for y false 2 false x − 4x + 3 < 0 test candidates for x −∞ ξ10 +ε ξ20 +ε virtually substituting text candidates for x false √ √ 5. Illustration for Example 25 with ξ1 = 2 −0 −x + 4x 2 Fig. √ − 3, ξ2 = 2 + −x2 + 4x √ − 3, sc1 = sc2 = (x − 4x + 3 < 0), ξ1 = 2 − 2/2 ≈ 1.29, and ξ20 = 2 + 2/2 ≈ 2.70. (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 (2) with the next formula (increasing i by 1) if there is any formula left to process (i.e., if i ≤ I); otherwise the algorithm terminates. 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 unsatisfiable. 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 conflict. But we could also continue the VS computations along the path that corre- sponds 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) = −∞. We virtually substitute this test candidate in ϕ2 , resulting in the formula false. Based on this VS com- putation we could learn the explanation (x − 2)2 + (y − 2)2 − 1 < 0 → ¬(x < ξ1 ). t u 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 satisfiability-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 different assignments, represented by the same path, which induce different orders over the test can- didates 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 define the path description D(ϕi,0 , . . . , ϕi,M ) to be D(ϕi,0 ) = ϕi for M = 0 and ∧M m=1 Ψ (ϕi,m−1 , ϕi,m ) otherwise. For the basic part, we propose three different definitions 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 = {t1 , . . . , tl , t01 , . . . , t0u } 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 , ∼0k ∈ {<, =} 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 )  sc(tl ) ∧ xi = tl  if l > 0 and ∼l is =  V  sc(t) ∧ V ¬sc(t)∧   t∈Ttrue t∈Tfalse  0 Vl−1 Vu−1 t < x ∧ x < t ∧ ( k=1 tk ∼k tk+1 ) ∧ ( k=1 t0k ∼0k t0k+1 )  l i i    1 if l > 0, u > 0 and ∼l is <     V V Vl−1 = t∈Ttrue sc(t) ∧ t∈Tfalse ¬sc(t) ∧ tl < xi ∧ ( k=1 tk ∼k tk+1 )      if l > 0, u = 0 and ∼l is <  V V 0 Vu−1 0 0 t∈Ttrue sc(t) ∧ t∈Tfalse ¬sc(t) ∧ xi < t1 ∧ ( k=1 tk ∼k tk+1 )          if l = 0 and u > 0  V t∈Tfalse ¬sc(t) else (if l = 0 and u = 0) Ψ2 (ϕi,m−1 , ϕi,m )   sc(tl ) ∧ xi = tl   if l > 0 and ∼l is = 0 0 → (t ≤ tl ∨ t01 ≤ t) V sc(t ) ∧ sc(t ) ∧ t < x ∧ x < t ∧ sc(t)  l l i i  1 1   t∈Tfalse ∪Ttrue      if l > 0, u > 0 and ∼l is < V = sc(tl ) ∧ tl < xi ∧ t∈Tfalse ∪Ttrue sc(t) → t ≤ tl      if l > 0, u = 0 and ∼l is < 0 0 0  V  sc(t1 ) ∧ xi < t1 ∧ t∈Tfalse ∪Ttrue sc(t) → t1 ≤ t if l = 0 and u > 0     V t∈Tfalse ¬sc(t) else (if l = 0 and u = 0) Ψ3 (ϕi,m−1 , ϕi,m )    sc(tl ) ∧ xi = tl if l > 0 and ∼l is =   sc(t ) ∧ t < x ∧ V  sc(t) → (t ≤ tl ∨ xi < t) l l i t∈Tfalse ∪Ttrue =   if l > 0 and ∼l is <  V  sc(t) → (x < t) else (if l = 0) t∈Tfalse ∪Ttrue i The formula Ψ1 provides the most strict description of why the current theory as- signment ν is not extensible, whereas Ψ2 and Ψ3 offer a more general explanation. More formally, (∃xi . ϕi,m−1 ∧ Ψ1 (ϕi,m−1 , ϕi,m )) → ϕi,m (∃xi . ϕi,m−1 ∧ Ψ2 (ϕi,m−1 , ϕi,m )) → ϕi,m (∃xi . ϕi,m−1 ∧ Ψ3 (ϕi,m−1 , ϕi,m )) ↔ ϕi,m and by the definition of D1 , D2 and D3 we get (∃x1 , . . . , xi . ϕi,0 ∧ D1 (ϕi,0 , . . . , ϕi,m )) → ϕi,m (∃x1 , . . . , xi . ϕi,0 ∧ D2 (ϕi,0 , . . . , ϕi,m )) → ϕi,m (∃x1 , . . . , xi . ϕi,0 ∧ D3 (ϕi,0 , . . . , ϕi,m )) ↔ ϕi,m Finally, let Π = {π1 , . . . , πk } 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 ∈ {D1 , D2 , D3 }. 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 for- malised more precisely, and proofs for the statements need to be given. After this step, we will develop a pseudo-algorithmic description of the explanation gener- ation for the VS method in the MCSAT context, and implement the approach based on our SMT solver SMT-RAT. Currently we work on the implementa- tion of the CAD embedding in MCSAT. Once that implementation is finished, 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 dif- ferent 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) efficiency. Though the MCSAT embedding of the CAD method in the Z3 SMT solver has been shown to be very efficient, we believe that harder arithmetic problems can be solved most efficiently by combinations of different decision procedures. To do so, we will use the possibilities offered 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. References 1. Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satis- fiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009) 2. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183. Springer (1975) 3. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962) 4. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (Jul 1960) 5. Gao, S., Ganai, M., Ivančić, 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 efficiency of a nonlinear-system-solver us- ing a componentwise Newton method. Tech. Rep. 2/1997, Inst. für Angewandte Mathematik, University of Karlsruhe (1997) 7. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Proc. of IJCAR’12. LNAI, vol. 7364, pp. 339–354. Springer (2012) 8. Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Proc. of VM- CAI’17. LNCS, vol. 10145, pp. 330–346. Springer (2017) 9. Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Proc. of FMCAD’13 (2013) 10. Košta, M.: New Concepts for Real Quantifier 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 satisfiability. IEEE Transactions on Computers 48, 506–521 (1999) 13. de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Proc. of VMCAI’13. pp. 1–12. Springer (2013) 14. Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997) 15. Zeljić, A., Wintersteiger, C.M., Rümmer, P.: Deciding bit-vector formulas with mcSAT. In: Proc. of SAT’16. pp. 249–266. Springer International Publishing (2016)