# Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection

arXiv: https://arxiv.org/abs/2003.00409 · HTML: https://mlsanity.com/paper/2003.00409/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Mar 2020.

## Built on by (most cited first, 1 of 1)

- [A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD](https://mlsanity.com/paper/2507.00557/) (2025)

## Abstract (arXiv)

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.