A Theory-Based Decision Heuristic for DPLL(T)

Dan Goldwasser     Ofer Strichman     Shai Fine    
Formal Methods in Computer-Aided Design (FMCAD), 2008


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.

Bib Entry

    author = "Dan Goldwasser and Ofer Strichman and Shai Fine",
    title = "A Theory-Based Decision Heuristic for DPLL(T)",
    booktitle = "Formal Methods in Computer-Aided Design (FMCAD)",
    year = "2008"