Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22616-8_27 | COCOA |
Keywords | Field | DocType |
tight integration,boolean combination,linear program,satisfiability modulo theories solver,nonlinear constraint,lp solver,interval arithmetic,interval constraint propagation,well-known dpll algorithm | Discrete mathematics,Local consistency,Nonlinear system,Computer science,Algorithm,DPLL algorithm,Solver,Interval arithmetic,Satisfiability modulo theories | Conference |
Volume | ISSN | Citations |
6831 | 0302-9743 | 1 |
PageRank | References | Authors |
0.37 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ernst Althaus | 1 | 257 | 26.33 |
| Bernd Becker | 2 | 855 | 73.74 |
| Daniel Dumitriu | 3 | 13 | 2.14 |
| Stefan Kupferschmid | 4 | 72 | 7.05 |