Name
Abstract | ||
|---|---|---|
We study the decision problem of disjunctive linear arithmetic over the reals from the perspective of computational geometry. We show that traversing the linear arrangement induced by the formula's predicates, rather than the DPLL(T) method of traversing the Boolean space, may have an advantage when the number of variables is smaller than the number of predicates (as it is indeed the case in the standard SMT-Lib benchmarks). We then continue by showing a branching heuristic that is based on approximating T-implications, based on a geometric analysis. We achieve modest improvement in run time comparing to the commonly used heuristic used by competitive solvers. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/FMCAD.2008.ECP.17 | FMCAD |
Keywords | Field | DocType |
computational geometry,decision problem,geometric analysis,approximating t-implications,theory-based decision heuristic,competitive solvers,run time,disjunctive linear arithmetic,modest improvement,boolean space,linear arrangement,boolean functions,approximation theory,benchmark testing,vectors,approximation algorithms,decision theory,linear systems,upper bound | Boolean function,Approximation algorithm,Heuristic,Decision problem,Linear system,Computer science,Computational geometry,Algorithm,DPLL algorithm,Decision theory | Conference |
Citations | PageRank | References |
5 | 0.52 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dan Goldwasser | 1 | 384 | 36.27 |
| Ofer Strichman | 2 | 1071 | 63.61 |
| Shai Fine | 3 | 1112 | 107.56 |