Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
Logic in Computer Science
2020-03-05 v2 Artificial Intelligence
Symbolic Computation
Abstract
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.
Cite
@article{arxiv.2003.00409,
title = {Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection},
author = {Haokun Li and Bican Xia},
journal= {arXiv preprint arXiv:2003.00409},
year = {2020}
}