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

Full work available at URL https://doi.org/10.1007/978-3-031-37703-7_5

zbMATH Keywords

cell-jumpcylindrical algebraic decompositionlocal searchnonlinear real arithmeticSMT

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• Improved projection for cylindrical algebraic decomposition
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Local search for Boolean satisfiability with configuration checking and subscore
• Local Search for SMT on Linear Integer Arithmetic
• 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
• raSAT: an SMT solver for polynomial constraints
• Solving non-linear arithmetic
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• The MathSAT5 SMT solver

Cited in

(3)

• A sampling-based method to estimate the volume of solution space for linear arithmetic constraints
• Boosting MCSat modulo nonlinear integer arithmetic via local search
• Breaking the data barrier in learning symbolic computation: a case study on variable ordering suggestion for cylindrical algebraic decomposition

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)