The research on SMT (Satisfiability Modulo Theories) [18,20,2] in recent years brings us many popular solvers such as Z3 [19], CVC4 [1], Yices [7], MathSAT5 [5], etc. Nevertheless, in theory and practice, it is important to design efficient SMT algorithms and develop tools (or improve existing ones) for many other theories, e.g. string [15], linear arithmetic [8,13] and non-linear arithmetic [3,14] over the reals. A straightforward idea is to integrate Conflict-Driven Clause Learning (CDCL)-style search with theory solvers [2]. For example, integrating CDCL-style search with a theory solver for determining whether a basic semialgebraic set is empty can solve satisfiability in the theory of non-linear arithmetic over the reals.

It is well-known that the problem whether a basic semialgebraic set is empty is decidable due to Tarski’s decision procedure [21]. Tarski’s algorithm cannot be a theory solver in practice because of its very high complexity. Cylindrical algebraic decomposition (CAD) algorithm [6] is a widely used theory solver in practice though it is of doubly exponential time complexity. The idea of CAD algorithm is to decompose into cells such that each polynomial from the problem is sign-invariant in every cell. A key concept in CAD algorithm is the projection operator. Although many improved projection operators have been proposed [11,16,17,4,10,9,22], the CAD method is still of doubly exponential time complexity. The main reason is that in order to carry enough information, projection of variables causes the number of polynomials grows rapidly. So the cost of simply using CAD as a theory solver is unacceptable.

Jovanovic and de Moura [13] eased the burden of using CAD as a theory solver by modifying the CDCL-style search framework. They changed the sequence of search states by adding variable assignments to the sequence. The benefit of this is that they can use real-root isolation, which is of polynomial time complexity, to check consistency of literals for there will be only one unassigned variable in the literals of the current state. When a conflict of literals is detected, they explain the conflict by applying CAD to a polynomial set called conflicting core to find the cell where the sample of assignments belongs. But even using CAD only when explaining conflicts is a huge computational cost, as CAD is of doubly exponential time complexity. Furthermore, CAD will produce all cells in other than the only one we need, making computation waste.

In this paper, we propose a new custom-made CAD-like projection operator, called sample-cell projection operator. It only processes the cell containing a given sample, which is exactly what conflict explanation needs. The idea of our operator is trying to project polynomials related to the target cell and ignore irrelevant polynomials. We integrate our sample-cell projection operator with Jovanovic’s improved CDCL-style search framework. The new operator can effi-ciently guide CDCL-style search away from conflicting states. It is proved that the new algorithm is of singly exponential time complexity. We have implemented a prototype solver LiMbS which is base on Mathematica 12. Experiments show the effectiveness of the new algorithm.

The rest of this paper is structured as follows: Section 2 introduces the background knowledge and notation. Section 3 defines sample-cell projection and presents the details of our approach. Section 4 describes the CDCL-style search framework which we adopt. We evaluate our approach on many well-known examples and analyze its performance in Section 5. The paper is concluded in Section 6.

Let R denote the field of real numbers, Z denote the ring of integers and Q denote the field of rational numbers. Unless stated otherwise, we assume that all polynomials in this paper are in ], the ring of multivariate polynomials in variables ¯x with integer coefficients.

For a polynomial ]:

where = 0 and ] for i = 0, ..., m, the degree of f with respect to (w.r.t.) x is m, denoted by deg(f, x). The leading coefficient of f w.r.t. x is , denoted by lc(f, x) and the leading term of f w.r.t. x is , denoted by lt(f, x). Let

where = 0 and ] for i = 0, ..., n . Let res(f, g, x) denote the Sylvester resultant of f and g w.r.t. x, i.e. the determinant of the following matrix

which has n rows of and m rows of . The discriminant of f w.r.t. x is

An atomic polynomial constraint is 0 where f is a polynomial and . A polynomial literal (simply literal) is an atomic polynomial constraint or its negation. For a literal l, poly(l) denotes the polynomial in l and var(l) = var(poly(l)). A polynomial clause is a disjunction of literals. Sometimes, we write a clause as . A polynomial formula is a conjunction of clauses. An extended polynomial constraint l is ) where ] with ) and )) is a given integer. Notice the variable u is an exclusive free variable that cannot be used outside the Root object.

For a formula ] denote the resulting formula via substituting a for x in . For variables ¯x = () and ¯a = (, a mapping which maps to for i = 1, ..., r is called a variable assignment of ¯x and ¯a is called a sample of or a sample of ¯x in . We denote ] by ). If ) = 0, we say vanishes under or vanishes under ¯a. Suppose an extended polynomial constraint l is of the form ) and is a variable assignment of (¯y, x). If is the kth real root of ) is defined to be . If ) has less than k real roots, ) is defined to be False.

In this section, we first introduce some well-known concepts and results concerning CAD and then define the so-called sample-cell projection operator.

Let f be an analytic function defined in some open set U of where K is a field. For a point , if f or some partial derivative (pure and mixed) of f of some order does not vanish at p, then we say that f has order r where r is the least non-negative integer such that some partial derivative of total order r does not vanish at p. Otherwise, we say f has infinite order at p. The order of f at p is denoted by . We say f is order-invariant in a subset if for any . Obviously, if K = R and the analytic function f is order-invariant in S, then f is sign-invariant in S.

An r-variable polynomial ) where ¯x = () is said to be analytic delineable on a connected s-dimensional submanifold if

1. The number k of different real roots of ) is invariant for any point . And the trace of the real roots are the graphs of some pairwise disjoint analytic functions from S into R (i.e. the order of real roots of ) is invariant for all point );

2. There exist positive integers such that for every point , the multiplicity of the real root ) of ) is for i = 1, ..., k.

Especially, if f has no zeros in , then f is delineable on S with k = 0. The analytic functions ’s are called the real root functions of f on S, the graphs of the ’s are called the f-sections over S, and the connected regions between two consecutive f-sections (for convenience, let and = +) are called f-sectors over S. Each f-section over S is a connected s-dimensional submanifold in and each f-sector over S is a connected (s + 1)-dimensional submanifold in .

Theorem 1 ([17], Theorem 2). Let 2 and ) be a polynomial in ] of positive degree where ¯x = (). Let S be a connect submanifold of where f is degree-invariant and does not vanish identically. Suppose that ) is a nonzero polynomial and is order-invariant in S. Then f is analytic delineable on S and is order-invariant in each f-section over S.

Suppose a = (¯) = () is a sample of (¯) in and F = is a polynomial set in ] where ¯x = (). Consider the real roots of polynomials in . Denote the kth real root of ) by . We define two concepts: the sample polynomials set of a in F (denoted by )) and the sample interval of a in F (denoted by )) as follows. If there exists such that then

If there exist two consecutive real roots and such that then

If there exists such that and for all then

If there exists such that and for all then

Specially, if every polynomial in does not have any real roots, define

Example 1. Let where 10, 01(7, 1 and A = (4, 9), B = (4, 6.75), C = (4, 4), D = (4, 1). We have (see Figure 1)

poly(F, y, A) = (F, y, A) = y > Root(f(x, u), 1), spoly(F, y, B) =

Fig. 1. Example 1

Additionally, for a polynomial

where ] and = 0 for i = 0, ..., m. If there exists 0 such that = 0 and ) = 0 for any i > j, then the sample coefficients of h at (¯) is defined to be , denoted by (¯)). Otherwise s

Definition 1. Suppose ¯a is a sample of ¯x in and is a polynomial set in ] where ¯x = (). The sample-cell projection of F on at ¯a is

– If and is obviously an element of ).

– Computing ) will produce O(rn + 3r) elements, so the time complexity of projecting all the variables by recursively using is O((n + 3)).

Now we prove the property of the new projection operator. A set of polynomials in ] is said to be a squarefree basis if the elements of the set have positive degrees, and are primitive, squarefree and pairwise relatively prime. For a connected submanifold S of , we denote by ) ]

Theorem 2. Let F be a finite squarefree basis in ] where ¯x = () and 2. Let ¯a = () be a sample of ¯x in and S be a connected submanifold of such that (. Suppose that each element of ) is order-invariant in S. Then each element in F either vanishes identically on S or is analytic delineable on S, each section over S of the element of F which do not vanish identically on S is either equal to or disjoint with ), and each element of F either vanishes identically on S or is order-invariant in ).

Proof. For any , if f vanishes identically on S, there is nothing to prove. So we may assume that any element in F does not vanish identically on S. For any such that ), let = .Notice that is degree-invariant on S (each element of ) is

order-invariant, hence sign-invariant in S). And we have

It follows from this equality that = 0 (because ’s are squarefree and pairwise relatively prime). Obviously, each factor of ) is a factor of ), so ) is order-invariant in S. By Theorem 1, is analytic delineable on S and is order-invariant in each -section over S. So f and ) are order-invariant in each -section over S. It follows that the sections over S of f and g are pairwise disjoint. Therefore, f and ) are analytic delineable on S, every section of them is either equal to or disjoint with ), and f and g are order-invariant in

Remark 2. Notice that when f vanishes identically on S, f isn’t always order-invariant in ). This is avoidable by changing the ordering of variables and is negligible when the satisfiability set of formulas is full-dimensional. We find a way to handle this rare case: either to determine whether the coefficients of f have finitely many common zeros, or to enlarge F by adding partial derivatives of f whose order is less than order(f) and one non-zero partial derivative whose order is exactly equal to order(f).

When integrating the new projection operator with the CDCL-type search (see Section 4), we need a traditional CAD projection operator [16,17].

Definition 2 ([16]). Suppose is a polynomial set in ] where ¯x = (). The McCallum projection of F on is

Remark 3. Notice that coeff can be replaced by scoeff when we have a sample of 1 dimension.

Theorem 3 ([17], Theorem 1). Let F be a finite squarefree basis in ] where ¯x = () and 2 and S be a connected submanifold of such that each element of ) is order-invariant in S. Then each element in F either vanishes identically on S or is analytic delineable on S, the sections over S of the elements of F which do not vanish identically on S are pairwise disjoint, and each element of F which does not vanish identically on S is order-invariant in every such section.

Now, let us use the following definition to describe the procedure of calculating sample cells. We denote by factor(A) the set of irreducible factors of all polynomials in A.

and is a polynomial set in ] where ¯x = (). The sample cell of F at a is

= a(F)))= (a, . . . , aF(F, x, αi = 1, . . . , n

– It is a standard way to use factor to ensure that every is a finite squarefree basis.

– Notice that the complexity of computing sample cell scell depends on where means the number of polynomials in . From the recursive relationship + (3 + i + 1)= 12, it is not hard to know that the complexity of computing scell is + rn)(2 + ).

Corollary 1. Let be a polynomial set and , where ¯x = (). If

Proof. It is a direct corollary of Theorem 3 and Theorem 2.

Example 2. Suppose + bx + c and = (1, 1, 1) is a sample of (a, b, c). Then

= factor(Proj)) = factor() = {a}, = factor(Proj)) = {a}.

and after simplification

In this section, we introduce a search framework combined with the new projection operator proposed in the previous section. The main notation and concepts about the search framework are taken from Section 3 of [13] and Section 26.4.4 of [2]. Let ¯x = () and ) = i. For a polynomial f, a literal l and a clause c, we define level(f) = max() = level(poly(l)) and level(c) = max(). We describe the search framework by transition relations between search states as in [13]. The search states are indexed pairs of the form , where is a finite set of polynomial clauses and M is a sequence of literals and variable assignments. Every literal is marked as a decision or a propagation literal. We denote a propagation literal l by if l is propagated from c and denote a decision literal l by . We denote by a variable assignment. Let ) = ) and v[M] = . For a set L of literals, v[M](L) means the resulting set of L after applying the assignments of v[M]. Next, we introduce transition relations between search states. Transition relations are specified by a set of transition rules. In the following, we use simple juxtaposition to denote the concatenation of sequences (). We treat a literal or a variable assignment as one-element sequence and denote the empty sequence as . We say the sequence M is ordered when the sequence is of the form M = []

where is a sequence of literals and each literal satisfies level(l) = j. Notice that might be . We define level(M) = k even if . We use sample(M) to denote the sample () of () in M and feasible(M) to denote the feasible set of ). For a new literal l with ), we say l is consistent with M if . If l is not consistent with M, we define core(l, M) to be a minimal set of literals L in M such that ) does not have a solution for .

Remark 5. Since there is only one unassigned variable in the polynomials in , so feasible(M) can be easily calculated by real-root isolation.

Definition 4. Suppose l is a literal and M is an ordered sequence which satisfies level(M) = level(l) and is not consistent with M. Define the explain clause of l with M as

Meanwhile, we define the state value of a literal l as

And for a clause c,

Specially, ) = False.

Definition 5. A set of rules for transition relations between search states are defined as follows where c is a clause and l is a literal.

Remark 6. Note that in this framework we rely on the rule lemma-propagation to guide the search away from conflicting states. When applying lemma-propagation, the most important thing is the explain clause. We cannot simply use the con-flicting core as the explain clause, as this will cause explain to be an incorrect lemma because it ignores assignments. Using full CAD to calculate explain is also costly. Thanks to the sample cell calculated by the novel sample-cell projection operator, we can now efficiently calculate an effective explain to achieve our purpose.

Theorem 4. Given a polynomial formula with finitely many clauses, any transition starting from the initial state will terminate either in a state (sat, v), where the assignment v satisfies the formula , or in the unsat state. In the later case, is unsatisfiable in R.

Proof. By Theorem 1 in [13], if there is a finite set such that all the literals returned every time by calling explain are always contained in the set, then the above theorem holds. On the other hand, it is not hard to see that all literals that may be generated by scell are determined by finitely many polynomials and their real roots and thus finite. That completes the proof.

In order to better demonstrate the effectiveness of our algorithm, we have implemented a prototype solver LiMbSwhich is base on Mathematica 12. The solver is a clean translation of the algorithm in this paper. Our solver is compared to the following solvers that have been popular in SMT nonlinear competition: Z3 (4.8.7-1), CVC4 (1.6-2), Yices (2.6.1) and MathSAT5 (5.6.0).

All tests were conducted on 6-Core Intel Core i7-8750H@2.20GHz with 32GB of memory and ARCH LINUX SYSTEM (5.5.4-arch1-1). The timeout is set to be 5 hours.

The examples listed below, which we collect from several related papers, are either special or cannot be well-solved by existing SMT solvers. All results are listed in Table 1.

where .

f(a+af +abcdebdf +af +2af + a3aef 3aef +3af +a+af +acef ab2abcf 4abcf 2abc+ 4abcef + 4abcef + abcd2abcef + abcf + abcabef + 2acdf + 2ac4acdef 2acde+ 2acdef + bf + 2bf + bcef cef 2bcdf 2bcdf + 2bcdef + cf + c+ cf + ccdcef < 0)

nr) Whether the distance between the ball ) and the complement of ) is less than ?

Our solver LiMbs solves all the 21 examples shown in Table 1. LiMbs is faster than the other solvers on 15 examples. Only LiMbs can solve 9 of the examples within a reasonable time while other solvers either run time out or return unknown state. From this we can see that our algorithm has great potential in solving satisfiability of polynomial formulas, especially considering that our prototype solver is a small program with less than 1000 lines of codes. For Hongn and Hong2n, though our solver is much faster than Z3, CVC4 is the one that performs best. We note that the examples of Hongn and Hong2n are all symmetric. This reminds us it is worth exploiting symmetry to optimize our solver’s performance.

Table 1. Comparison with other solvers on 21 examples

A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point is that we design a new projection operator, the sample-cell projection operator, which can efficiently guide CDCL-style search away from conflicting states. Preliminary evaluation of the prototype solver LiMbS shows the effectiveness of the new algorithm.

We will further develop our algorithm, looking into problems with symmetry, equations or other special structures. We also hope to develop an easy-to-use, robust and concise open-source algorithm framework based on our prototype solver to achieve a wider range of applications.

This work was supported partly by NSFC under grants 61732001 and 61532019.

1. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi’c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11). pp. 171–177 (2011)

2. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

3. Brauße, F., Korovin, K., Korovina, M.V., M¨uller, N.T.: A cdcl-style calculus for solving non-linear constraints (2019), http://arxiv.org/abs/1905.09227

4. Brown, C.W.: Improved Projection for Cylindrical Algebraic Decomposition. Jour- nal of Symbolic Computation 32(5), 447–465 (2001)

5. Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) Proceedings of TACAS. LNCS, vol. 7795, pp. 93–107. Springer (2013)

6. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages, LNCS 33. pp. 134– 183 (1975)

7. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification (CAV’2014). LNCS, vol. 8559, pp. 737–744. Springer (2014)

8. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of CAV 2006. pp. 81–94 (2006)

9. Han, J., Dai, L., Hong, H., Xia, B.: Open weak cad and its applications. Journal of Symbolic Computation 80, 785–816 (2017)

10. Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in cad projection. In: Proceedings of ISSAC’14. pp. 240–247 (2014)

11. Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of ISSAC ’90, 1990. pp. 261–264 (1990)

12. Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Tech. rep. (1991)

13. Jovanovic, D., de Moura, L.M.: Solving non-linear arithmetic. In: Automated Reasoning - 6th International Joint Conference, IJCAR 2012. pp. 339–354 (2012)

14. Korovin, K., Kosta, M., Sturm, T.: Towards conflict-driven learning for virtual substitution. In: Proceedings of SMT 2014. p. 71 (2014)

15. Liang, T., Reynolds, A., Tinelli, C., Barrett, C.W., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Proceedings of CAV 2014. pp. 646–662 (2014)

16. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symb. Comput. 5(1/2), 141–161 (1988)

17. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. pp. 242–268. Springer Vienna, Vienna (1998)

18. de Moura, L., Dutertre, B., Shankar, N.: A tutorial on satisfiability modulo theo- ries. In: Proceedings of CAV’2007. LNCS, vol. 4590, pp. 20–36 (2007)

19. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. pp. 337–340 (2008)

20. de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

21. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)

22. Xia, B., Yang, L.: Automated Inequality Proving and Discovering. WORLD SCI- ENTIFIC (Aug 2016)