 |
    |
A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition*
Ulrich Loup1, Karsten Scheibler2, Florian Corzilius1, Erika Ábrahám1, and Bernd Becker2
1RWTH Aachen University, Germany
2University of Freiburg, Germany
Abstract. We present a novel decision procedure for non-linear real arithmetic: a combination of iSAT, an incomplete SMT solver based on interval constraint propagation (ICP), and an implementation of the complete cylindrical algebraic decomposition (CAD) method in the library GiNaCRA . While iSAT is efficient in finding unsatisfiability, on satisfiable instances it often terminates with an interval box whose satisfiability status is unknown to iSAT. The CAD method, in turn, always terminates with a satisfiability result. However, it has to traverse a double-exponentially large search space.
A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search “tube” rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions.
*This work has been partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “AVACS” (SFB/TR 14, http://www.avacs.org/ and the Research Training Group “AlgoSyn” (GRK 1298, http://www.algosyn.rwth-aachen.de/)
LNAI 7898, p. 193 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013