PolyQEnt: A Polynomial Quantified Entailment Solver
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, Đorđe Žikelić
TL;DR
PolyQEnt tackles polynomial quantified entailments of the form $\exists t \in \mathbb{R}^m.\, \bigwedge_{i=1}^K (\forall x \in \mathbb{R}^n.\, \Phi^i(x,t) \Rightarrow \Psi^i(x,t))$, where $\Phi^i$ and $\Psi^i$ are boolean combinations of polynomial inequalities. It introduces a canonicalization step and leverages positivity theorems—Farkas' lemma, Handelman’s theorem, and Putinar’s theorem—to reduce the universal quantification to an existential polynomial constraint system that can be fed to SMT solvers like Z3 or MathSAT. The paper provides a detailed architecture, a configurable workflow, and two heuristics (Assume-SAT and UNSAT-core) and demonstrates substantial empirical gains over direct SMT solving across termination, almost-sure termination, and synthesis benchmarks, while also discussing solver choices and parallelization. Overall, PolyQEnt offers a modular, scalable approach to PQE solving that decouples certificate design from constraint solving, with practical impact for verification and program-analysis pipelines.
Abstract
Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.