Integration of DPLL and Interval Constraint Solving

Abstract

Having dealt with Boolean combinations of linear arithmetic constraints in the previous chapter, we now address the problem of solving Boolean combinations of nonlinear arithmetic constraints which may contain transcendental functions, like sine, cosine, and the exponential function. This gives rise to a plethora of problems, in particular (a) how to efficiently and sufficiently completely solve conjunctive combinations of constraints in the undecidable domain of nonlinear constraints involving transcendental functions and (b) how to efficiently maneuver the large search spaces arising from the potentially rich Boolean structure of the overall formula.