2010/01/01 by Erika Ábrahám, Ulrich Loup, Abraham, Erika +1
Computer Science · Mathematics · #Artificial intelligence #Backtracking #Computer science #Decidability #Embedding #Focus (optics) #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Order (exchange) #Programming language #SMT-solving #Satisfiability #Satisfiability modulo theories #Solver #Theoretical computer science #first-order theory of the reals #verification
paper · doi:10.4230/dagsemproc.09461.3
published in DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 0 (Schloss Dagstuhl – Leibniz Center for Informatics)
openalex publication_date 2010/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
SAT-solving is a highly actual research area with increasing success and plenty of industrial applications. SMT-solving, extending SAT with theories, has its main focus on linear real constrains. However, there are only few solvers going further to more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication. The main requests on theory solvers that must be fulfilled for their efficient embedding into an SMT solver are (a) incrementality, (b) the efficient computation of minimal infeasible subsets, and (c) the support of backtracking. For the first-order theory of the reals we are not aware of any solver offering those functionalities. In this work we address the possibilities to extend existing theory solving algorithms to come up with a theory solver suited for SMT.