Interval Constraint Propagation in SMT Compliant Decision Procedures
Stefan Schupp, Erika Ábrahám, Peter Rossmanith, Ulrich Loup, Florian Corzilius · 2013
There is a wide range of decision procedures available for solving the existential fragment of first order theory of linear real algebra (QFLRA). However, for formulas of the theory of quantifier-free nonlinear real arithmetic (QFNRA), which are much harder to solve, there are only few decision procedures (the lower bound for complete solvers is exponential). The context this thesis is settled in is the software project SMT-RAT, a software framework for SAT Modulo Theories (SMT) solving. SMT solving is a combination of a SAT solver, which checks the Boolean skeleton of a given input formula and a theory solver, which handles the involved theory constraints. SMT-RAT maintains different complete and incomplete solving modules and allows to combine several modules to operate as a theory solver. Interval constraint propagation (ICP) is an incomplete decision procedure to efficiently reduce the domain of a set of variables with respect to a conjunction of polynomial constraints. The goal of this thesis is to present a module based on ICP for SMT-RAT. This module takes a conjunction of polynomial constraints as well as an initial set of boundaries, represented by intervals, for the variables occurring in the constraints as an input. It utilizes an interval extension of Newton’s method to reduce the domain of the given variables up to a certain bound and passes the set of constraints as well as the new boundaries to complete solvers, such as the module based on the cylindrical algebraic decomposition (CAD).