Interval Constraint Solving Using Propositional SAT Solving Techniques

Abstract. In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we extend the paradigm of lazy theorem proving to intervalbased arithmetic constraint solving. Algorithmically, our approach deviates substantially from “classical ” lazy theorem proving approaches in that it directly controls arithmetic con…