A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition

Ulrich Loup (Hybrid Systems)

other hand, our work is a tight combination of two methods to solve non-linear real-arithmetic formulas, each having drawbacks, but being very powerful when combined.The first method is based on interval-constraint propagation (ICP) and is implemented in the satisfiability-modulo-theories (SMT) solver iSAT developed in Freiburg. In this approach, interval arithmetic is used in order to contract initial bounds to the input variables until either unsatisfiability is deduced or the interval size is below a certain threshold. In that case, the method terminates with an interval box whose satisfiability status is unknown to iSAT.

The other method, in turn, always terminates with a satisfiability result: the cylindrical algebraic decomposition (CAD) method, a procedure being able to construct one representative for every maximal connected component of the

solution space where the input formula does not change its truth value. However, the number of these representatives is doubly exponential in the number of input variables.

A symbiosis of iSAT and our CAD implementation 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 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, as it is currently pursued in Microsoft’s solver Z3.