Integration of DPLL and Interval Constraint Solving

  • Christian Herde


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.


Bound Model Check Deduction Rule Theory Atom Interval Constraint Error Trace 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Vieweg+Teubner Verlag | Springer Fachmedien Wiesbaden GmbH 2011

Authors and Affiliations

  • Christian Herde

There are no affiliations available

Personalised recommendations