More is less: adding polynomials for faster explanations in NLSAT

DOI10.1007/978-3-031-99984-0_7MaRDI QIDQ6869959zbMATH OpenFDO

Authors Valentin Promies, Jasper Nalbach, Erika Ábrahám, P. Wagner

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_7

zbMATH Keywords

cylindrical algebraic decompositionreal algebrasingle cell constructionSMT solving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• A CDCL-style calculus for solving non-linear constraints
• A model-constructing satisfiability calculus
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Constructing a single cell in cylindrical algebraic decomposition
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• dReal: an SMT solver for nonlinear theories over the reals
• Efficient projection orders for CAD
• Extending Sledgehammer with SMT solvers
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 589124 (Why is no real title available?)
• Improved projection for cylindrical algebraic decomposition
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Levelwise construction of a single cylindrical algebraic cell
• Merging adjacent cells during single cell construction
• Minimal Conjunctive Normal Expression of Continuous Piecewise Affine Functions
• Satisfiability modulo theories
• Solving non-linear arithmetic
• Ueber eine zahlentheoretische Funktion.

This page was built for publication: More is less: adding polynomials for faster explanations in NLSAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869959)