Integration of an LP Solver into Interval Constraint Propagation
Integration of an LP Solver into Interval Constraint Propagation
复制标题
将 LP 求解器集成到区间约束传播中
DOI：
10.1007/978-3-642-22616-8_27
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Stefan Kupferschmid
中科院分区：
文献类型：
--
作者：
Ernst Althaus;B. Becker;D. Dumitriu;Stefan Kupferschmid
本文介绍了一个LP求解器集成到iSAT，可满足性模理论求解器，可以解决线性和非线性约束的布尔组合。iSAT是众所周知的DPLL算法和区间约束传播的紧密集成，允许其推理线性和非线性约束。由于区间算法在求解线性规划时效率较低，我们将演示如何集成LP求解器来提高iSAT的整体求解性能。
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.