Research map / Learning theory and algorithms / Combinatorial and search optimization
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes QuantiSAT, a template-based Skolemization method that eliminates quantifiers in LRA/NRA formulas via Positivstellensatz-based reduction to quantifier-free polynomial constraints, yielding sound, semi-complete, subexponential-time, polynomial-space satisfiability checking with witnesses.
Problem
Checking satisfiability of quantified linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas, where existing sound and complete quantifier elimination is doubly-exponential and existing approaches are incomplete or LRA-only.
Approach
Replace each existentially quantified variable by a symbolic linear/polynomial Skolem template over preceding universal variables, then eliminate universal quantifiers using Farkas' lemma, Handelman's theorem, or Putinar's Positivstellensatz, yielding a quantifier-free system solved by an SMT solver; the solution directly gives Skolem witnesses.
Key results
- On Mjollnir LRA benchmarks QuantiSAT solves 877 instances versus 593 for the best baseline Z3-tSk (Z3-uSk: 476), with 157 unique solutions.
- On Keymaera NRA benchmarks QuantiSAT solves 503 instances versus 483 for the best baseline Z3-tSk, including 22 unique instances.
- On PolySynth NRA benchmarks QuantiSAT solves 30 instances versus 28 for Z3-tSk, with 4 unique instances and lower average runtime than Z3-tSk.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · Keymaera-LRA | solved instances: 222 -> 222 | No clear effect |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · Mjollnir | solved instances: 593 -> 877 | Helped |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · Mjollnir | average runtime (s): 23.34 -> 18.48 | Helped |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · Keymaera-NRA | solved instances: 483 -> 503 | Helped |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · Keymaera-NRA | average runtime (s): 0.03 -> 0.06 | Hurt |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · PolySynth | solved instances: 28 -> 30 | Helped |
| Use QuantiSAT instead of Z3-tSk | Quantified satisfiability checking · PolySynth | average runtime (s): 11.16 -> 4.00 | Helped |
Surprising findings
- Z3 with uninterpreted Skolem functions solves 76 Mjollnir instances that QuantiSAT cannot, requiring heavily piecewise Skolem functions outside polynomial templates.
Limitations
- Semi-completeness only holds for Skolem functions within the chosen polynomial template degree D; piecewise Skolem functions are not covered.
- Requires quantifier-free part in CNF as input; CNF conversion time excluded from reported runtimes.
Experimental setup
Datasets: Keymaera benchmark suite (SMT-COMP) Mjollnir benchmark suite PolySynth benchmark suite
Benchmarks: Keymaera LRA Keymaera NRA Mjollnir PolySynth
Metrics: number of solved instances average runtime unique solved instances
Baselines: Z3-uSk Z3-tSk CVC5-tSk
Builds on: Farkas' lemma Handelman's theorem Putinar's Positivstellensatz Krivine-Stengle Positivstellensatz PolyHorn
Closest papers by meaning
- Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.85)
- A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic (AAAI 2025 · similarity 0.84)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.83)
- Computationally Hard Problems Are Hard for QBF Proof Systems Too (AAAI 2025 · similarity 0.82)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.82)
- A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract) (AAAI 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.