A Survey of Satisfiability Modulo Theory <s> Conclusion <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> Conclusion <s> A sweep auger radially mounted within a storage bin is rotatable horizontally across the bin floor about a vertical axis located centrally of the bin. An upright distributing auger arranged coaxially with the vertical axis has its lower end adjacent the inner end of the sweep auger and its upper end spaced from the roof of the bin. The sweep auger is of a construction such that for each complete revolution across the bin floor it moves predetermined volumes of material over given axial sections thereof for delivery to the distributing auger. The material or grain discharged from the distributing auger is spread across the top surface of the grain stored in the bin. All of the grain in the bin is thus acted upon continuously for circulation through the bin for drying purposes. Field grain may be introduced through the roof of the bin for concurrent distribution and circulation with the grain already in the bin. A bin unloading auger is located below the bin floor to receive grain directly from the sweep auger for discharge exteriorly of the bin. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Conclusion <s> Algebraically Closed Fields.- Real Closed Fields.- Semi-Algebraic Sets.- Algebra.- Decomposition of Semi-Algebraic Sets.- Elements of Topology.- Quantitative Semi-algebraic Geometry.- Complexity of Basic Algorithms.- Cauchy Index and Applications.- Real Roots.- Cylindrical Decomposition Algorithm.- Polynomial System Solving.- Existential Theory of the Reals.- Quantifier Elimination.- Computing Roadmaps and Connected Components of Algebraic Sets.- Computing Roadmaps and Connected Components of Semi-algebraic Sets. <s> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Conclusion <s> Let f 1 , ldots, f s be polynomials in Q[X 1 , ..., X n ] that generate a radical ideal and let V be their complex zero-set. Suppose that V is smooth and equidimensional; then we show that computing suitable sections of the polar varieties associated to generic projections of V gives at least one point in each connected component of V ∩ Rn. We deduce an algorithm that extends that of Bank, Giusti, Heintz and Mbakop to non-compact situations. Its arithmetic complexity is polynomial in the complexity of evaluation of the input system, an intrinsic algebraic quantity and a combinatorial quantity. <s> BIB004 </s> A Survey of Satisfiability Modulo Theory <s> Conclusion <s> SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework allows for a degree of modularity in the treatment of theory solvers. Over time, theory solvers have become more and more closely integrated into the DPLL process, and consequently less and less modular. In this paper, we present a DPLL-like algorithm for SMT solving in which the search takes place over the natural domain of the variables in the problem. As a case study, we analyze its application to continuous domain linear arithmetic, present implementation techniques and some experimentation with difference logic. Results indicate the method can sometimes outperform leading SMT solvers but that the method is not yet robust. <s> BIB005 </s> A Survey of Satisfiability Modulo Theory <s> Conclusion <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> BIB006 </s> A Survey of Satisfiability Modulo Theory <s> Conclusion <s> Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. <s> BIB007
Considerable progress has been made within the last 15 years on increasingly practical decision procedures for increasingly large classes of formulas, even though worst-case complexity is prohibitive, and sometimes even though the class is undecidable. BIB005 Major ingredients to that success were i) lazy generation of lemmas, partial projections or instantiations, guided by counterexamples (as opposed to eager exhaustive generation, often explosive) ii) generalization of counterexamples so as to learn sufficiently general blocking lemmas iii) tight integration of propositional and theory-specific reasoning. Nonlinear arithmetic reasoning (polynomials, or even transcendental functions) is still a very open question. Current approaches in SMT BIB006 are based on partial cylindrical algebraic decomposition BIB001 ; possibly methods based on critical points BIB003 BIB002 BIB004 could be investigated as well. There are several challenges to using computer algebra procedures inside a SMT solver. i) These procedures may not admit addition or retraction of constraints without recomputation. ii) They may compute eagerly large sets of formulas (as in conventional cylindrical algebraic decomposition). iii) They may be very complex and thus likely to contain bugs. BIB007 Being able to produce independently-checkable proof witnesses would help in this respect.