=Paper=
{{Paper
|id=Vol-1974/EAb
|storemode=property
|title=Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
|pdfUrl=https://ceur-ws.org/Vol-1974/EAb.pdf
|volume=Vol-1974
|authors=Erika Abraham,Jasper Nalbach,Gereon Kremer
|dblpUrl=https://dblp.org/rec/conf/issac/AbrahamNK17
}}
==Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework==
https://ceur-ws.org/Vol-1974/EAb.pdf
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)