A Theory-Based Decision Heuristic for Disjunctive Linear Arithmetic
Dan L. Goldwasser · 2008
This work studies the decision problem of Disjunctive Linear Arithmetic over the Reals from the perspective of computational geometry. Given a formula, the geometric search space can be defined as the set of d -cells in a linear hyperplane arrangement induced by the formula’s predicates. We show that traversing this space, rather than the Boolean space as done by current approaches, 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 used for evaluation by the research community). 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.