6533b7ddfe1ef96bd1273c57

RESEARCH PRODUCT

Integration of an LP Solver into Interval Constraint Propagation

Bernd BeckerDaniel DumitriuErnst AlthausStefan Kupferschmid

subject

Nonlinear systemSatisfiability modulo theoriesDPLL algorithmLocal consistencyBoolean combinationInterval (mathematics)SolverAlgorithmMathematicsInterval arithmetic

description

This paper describes the integration of an LP solver into iSAT, a Satisfiability Modulo Theories solver that can solve Boolean combinations of linear and nonlinear constraints. iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation allowing it to reason about linear and nonlinear constraints. As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT.

yearjournalcountryeditionlanguage
2011-01-01
https://doi.org/10.1007/978-3-642-22616-8_27