Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
This addresses a computational bottleneck in automated theorem proving and formal verification, representing an incremental improvement over existing CAD-based methods.
The paper tackles the problem of deciding satisfiability of polynomial formulas over the reals by introducing a new sample-cell projection operator that efficiently guides CDCL-style search, achieving singly exponential time complexity and showing effectiveness in experiments.
A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.