{'fraction_non_alphanumeric': 0.058844194624978044, 'fraction_numerical': 0.011241875988055507, 'mean_word_length': 3.778959149412423, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 13, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection

A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.


Introduction
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 R n 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 R n 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 efficiently 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.

Notation
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 Z[x], the ring of multivariate polynomials in variablesx with integer coefficients.
For a polynomial f ∈ Z[ȳ, x]: denote the set of coefficients of f w.r.t.
x and var(f ) = {ȳ, x} denote the variables appearing in f . Suppose g ∈ Z[ȳ, x]: 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 An atomic polynomial constraint is f ⊲ 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 l 1 ∨ · · · ∨ l s of literals. Sometimes, we write a clause as ¬( i l i ) ∨ j l j . A polynomial formula is a conjunction of clauses. An extended polynomial constraint l is x ⊲ Root(f, k) where ⊲ ∈ {≥, >, =}, f ∈ Z[ȳ, u] with x ∈ var(f ) and k(0 ≤ k ≤ deg(f, u)) is a given integer. Notice the variable u is an exclusive free variable that cannot be used outside the Root object.
For a formula φ, φ[a/x] denote the resulting formula via substituting a for x in φ. For variablesx = (x 1 , . . . , x r ) andā = (a 1 , . . . , a r ) ∈ R r , a mapping α which maps x i to a i for i = 1, ..., r is called a variable assignment ofx andā is called a sample of α or a sample ofx in R r . We denote φ[a 1 /x 1 , . . . , a r /x r ] by α(φ). If α(φ) = 0, we say φ vanishes under α or vanishes underā. Suppose an extended polynomial constraint l is of the form x ⊲ Root(f, k) and α is a variable assignment of (ȳ, x). If β k is the kth real root of α(f ), α(l) is defined to be α(x) ⊲ β k . If α(f ) has less than k real roots, α(l) is defined to be False.

Sample-Cell Projection
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 K n where K is a field. For a point p ∈ U , 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 And the trace of the real roots are the graphs of some pairwise disjoint analytic functions θ 1 < . . . < θ k from S into R (i.e. the order of real roots of f (a, x r ) is invariant for all point a ∈ S); 2. There exist positive integers m 1 , . . . , m k such that for every point a ∈ S, the multiplicity of the real root Especially, if f has no zeros in S × R, then f is delineable on S with k = 0. The analytic functions θ i 's are called the real root functions of f on S, the graphs of the θ i 's are called the f -sections over S, and the connected regions between two consecutive f -sections (for convenience, let θ 0 = −∞ and θ k+1 = +∞) are called f -sectors over S. Each f -section over S is a connected s-dimensional submanifold in R r and each f -sector over S is a connected (s + 1)-dimensional submanifold in R r . Suppose a = (ā, a n ) = (a 1 , . . . , a n ) is a sample of (x, x n ) in R n and F = Consider the real roots of polynomials in {f 1 (ā, x n ), . . . , f r (ā, x n )} \ {0}. Denote the kth real root of f i (ā, x n ) by θ i,k . We define two concepts: the sample polynomials set of a in F (denoted by s poly(F, x n , a)) and the sample interval of a in F (denoted by s interval(F, x n , a)) as follows.
-Computing Proj sc (F, x n ,ā) will produce O(rn + 3r) elements, so the time complexity of projecting all the variables by recursively using Proj sc is O((n + 3) n r).
Now we prove the property of the new projection operator. A set of polynomials in Z[x] 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 R n−1 , we denote by S × s interval(F, x n ,ā) (α 1 , . . . , α n ) ∈ R n | (α 1 , . . . , α n−1 ) ∈ S ∧ s interval(F, x n ,ā)[α 1 /x 1 , . . . , α n /x n ] .
Theorem 2. Let F be a finite squarefree basis in Z[x] wherex = (x 1 , . . . , x n ) and n ≥ 2. Letā = (a 1 , . . . , a n ) be a sample ofx in R n and S be a connected submanifold of R n−1 such that (a 1 , . . . , a n−1 ) ∈ S. Suppose that each element of Proj sc (F, x n ,ā) 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 S × s interval(F, x n ,ā), and each element of F either vanishes identically on S or is order-invariant in S × s interval(F, x n ,ā).
Proof. For any f ∈ F , 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 f ∈ F such that f ∈ s poly(F, x n ,ā), let f ′ = f · g∈s poly(F,xn,ā) g. Notice that f ′ is degree-invariant on S (each element of s coeff(f, x n ,ā) is order-invariant, hence sign-invariant in S). And we have disc(f ′ , x n ) = disc(f, x n ) · g∈s poly(F,xn,ā) disc(g, x n )· g∈s poly(F,xn,ā) res(f, g, x n )· g1∈s poly(F,xn,ā), g2∈s poly(F,xn,ā), g1 =g2 res(g 1 , g 2 , x n ).
It follows from this equality that disc(f ′ , x n ) = 0 (because f i 's are squarefree and pairwise relatively prime). Obviously, each factor of disc(f ′ , x n ) is a factor of Proj sc (F, x n ,ā), so disc(f ′ , x n ) is order-invariant in S. By Theorem 1, f ′ is analytic delineable on S and is order-invariant in each f ′ -section over S. So f and g ∈ s poly(F, x n ,ā) are order-invariant in each f ′ -section over S. It follows that the sections over S of f and g are pairwise disjoint. Therefore, f and g ∈ s poly(F, x n ,ā) are analytic delineable on S, every section of them is either equal to or disjoint with S × s interval(F, x n ,ā), and f and g are order-invariant in S × s interval(F, x n ,ā).

Remark 2.
Notice that when f vanishes identically on S, f isn't always orderinvariant in S × s interval(F, x n ,ā). 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]. 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. a = (a 1 , . . . , a n−1 ) is a sample of (x 1 , . . . , x n−1 ) in R n−1 and

Remark 4.
-It is a standard way to use factor to ensure that every F i is a finite squarefree basis. -Notice that the complexity of computing sample cell s cell depends on . . , n − 2, it is not hard to know that the complexity of computing s cell is O((r 2 + rn)(2 + n) n−1 ).
Proof. It is a direct corollary of Theorem 3 and Theorem 2.
Example 2. Suppose f = ax 2 + bx + c and α = (1, 1, 1) is a sample of (a, b, c). Then 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]. Letx = (x 1 , . . . , x n ) and level(x i ) = i. For a polynomial f , a literal l and a clause c, we define level(f ) = max({level(a)|a ∈ var(f ))}, level(l) = level(poly(l)) and level(c) = max({level(l)|l ∈ c}). We describe the search framework by transition relations between search states as in [13].
The search states are indexed pairs of the form M ζ, 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 c → l if l is propagated from c and denote a decision literal l by l • . We denote by x i → a i a variable assignment. Let level( 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 (e.g., M, M ′ ). 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 where N j is a sequence of literals and each literal l ∈ N j satisfies level(l) = j. Notice that N j might be ∅. We define level(M ) = k even if N k = ∅. We use sample(M ) to denote the sample (a 1 , . . . , a k−1 ) of (x 1 , . . . ,  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 conflicting 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 s cell are determined by finitely many polynomials and their real roots and thus finite. That completes the proof.

Experiments
In order to better demonstrate the effectiveness of our algorithm, we have implemented a prototype solver LiMbS 2 which 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.
Hong n ∃x 1 , . . . , ∃x n n i=1 Hong2 n x i > 1 Example 6. (C n r) Whether the distance between the ball B r (x) and the complement of B 8 (x) is less than 1 1000 ?
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 Hong n and Hong2 n, though our solver is much faster than Z3, CVC4 is the one that performs best. We note that the examples of Hong n and Hong2 n are all symmetric. This reminds us it is worth exploiting symmetry to optimize our solver's performance.

Conclusions
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.