Interval Constraint Propagation in Smt Compliant Decision Procedures

The goal of this thesis is to present a module based on ICP for SMT-RAT, a software framework for SAT Modulo Theories solving that takes a conjunction of polynomial constraints as well as an initial set of boundaries for the variables occurring in the constraints as an input. 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.