Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection

2020/03/01 by Li, Haokun, Xia, Bican · 2 citations
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Symbolic Computation (cs.SC)

paper · doi:10.48550/arxiv.2003.00409

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.

Cited by

• More is Less: Adding Polynomials for Faster Explanations in NLSAT
• A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD

Related

• Local Search for Solving Satisfiability of Polynomial Formulas
• More is Less: Adding Polynomials for Faster Explanations in NLSAT
• Better algorithms for satisfiability problems for formulas of bounded\n rank-width
• A Real World Mechanism for Testing Satisfiability in Polynomial Time
• Exploiting Strict Constraints in the Cylindrical Algebraic Covering