A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition

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.