Name
Title | ||
|---|---|---|
Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure |
Abstract | ||
|---|---|---|
In order to facilitate automated reasoning about large Boolean combinations of non- linear arithmetic constraints involving transcendental functions, we provide a tight inte- gration of recent SAT solving techniques with interval-based arithmetic constraint solv- ing. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than del- egating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving carry over smoothly to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combina- tions of multiple thousand arithmetic constraints over some thousands of variables. |
Year | Venue | Keywords |
|---|---|---|
2007 | JSAT | interval-based arithmetic constraint solving,sat modulo theories,theorem proving,constraint propagation,automated reasoning,sat solver |
Field | DocType | Volume |
Automated reasoning,Discrete mathematics,Local consistency,Affine arithmetic,Transcendental function,Automated theorem proving,Boolean satisfiability problem,Arithmetic,Theoretical computer science,Solver,Mathematics,Satisfiability modulo theories | Journal | 1 |
Issue | Citations | PageRank |
3-4 | 150 | 5.86 |
References | Authors | |
19 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Fränzle | 1 | 786 | 61.58 |
| Christian Herde | 2 | 338 | 15.19 |
| Tino Teige | 3 | 258 | 17.56 |
| stefan ratschan | 4 | 476 | 28.75 |
| Tobias Schubert | 5 | 598 | 37.74 |