Local search for solving satisfiability of polynomial formulas

DOI10.1007/978-3-031-37703-7_5MaRDI QIDQ6535529zbMATH OpenFDO

Authors Haokun Li, Bican Xia, Tianqi Zhao

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

local searchSMTcylindrical algebraic decompositionnonlinear real arithmeticcell-jump

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• raSAT: An SMT Solver for Polynomial Constraints
• Subtropical satisfiability
• raSAT: an SMT solver for polynomial constraints
• Local Search for SMT on Linear Integer Arithmetic
• A search-based procedure for nonlinear real arithmetic

Cites work

• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 1302201 (Why is no real title available?)
• scientific article; zbMATH DE number 589124 (Why is no real title available?)
• scientific article; zbMATH DE number 1157658 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A model-constructing satisfiability calculus
• Choosing probability distributions for stochastic local search and the role of make versus break
• Computer Aided Verification
• 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
• Handbook of model checking
• Improved projection for cylindrical algebraic decomposition
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Local Search for SMT on Linear Integer Arithmetic
• Local search for Boolean satisfiability with configuration checking and subscore
• Partial cylindrical algebraic decomposition for quantifier elimination
• Precise and complete propagation based local search for satisfiability modulo theories
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Solving non-linear arithmetic
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• The MathSAT5 SMT solver
• raSAT: an SMT solver for polynomial constraints

This page was built for publication: Local search for solving satisfiability of polynomial formulas

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