A Survey of Satisfiability Modulo Theory <s> Nonlinear Arithmetic (NRA) <s> Tarski in 1948, (Tarski 1951) published a quantifier elimination method for the elementary theory of real closed fields (which he had discovered in 1930). As noted by Tarski, any quantifier elimination method for this theory also provides a decision method, which enables one to decide whether any sentence of the theory is true or false. Since many important and difficult mathematical problems can be expressed in this theory, any computationally feasible quantifier elimination algorithm would be of utmost significance. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Nonlinear Arithmetic (NRA) <s> We present a new algorithm for deciding satisfiability of non-linear arithmetic constraints. The algorithm performs a Conflict-Driven Clause Learning (CDCL)-style search for a feasible assignment, while using projection operators adapted from cylindrical algebraic decomposition to guide the search away from the conflicting states. <s> BIB002
The MCSAT approach can also be applied to polynomial real arithmetic. Again, the problem is: assuming a set of polynomial constraints over x 1 , . . . , x n , x n+1 have no solution over x n+1 for a given valuation v(x 1 ), . . . , v(x n ), how can we explain this impossibility by a system of constraints over x 1 , . . . , x n that excludes v(x 1 ), . . . , v(x n ) and hopefully many more? Jovanović and de Moura BIB002 proposed applying a modified version of Collin's BIB001 projection operator in order to perform a partial cylindrical algebraic decomposition. In that approach, known as NLSAT, one additional difficulty is that assignments to variables may refer to algebraic reals, and thus the system needs to compute to compute over algebraic reals, including as coefficients to polynomials. It is yet unknown whether this approach could benefit from using other projection operators such as Hong's  or McCallum's  . 4 Beyond Quantifier-Free Decidability