# PolyQEnt: A Polynomial Quantified Entailment Solver

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Aug 2024.

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

- [Automated Approach for Solving Infinite-state Polynomial Reachability Games](https://mlsanity.com/paper/2605.10169/) (2026)
- [Entropy Objectives in Markov Decision Processes](https://mlsanity.com/paper/2606.21726/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

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.