Local search for solving satisfiability of polynomial formulas

DOI10.1007/978-3-031-37703-7_5zbMATH Open1545.68122MaRDI QIDQ6535529

Haokun Li, Tianqi Zhao, Bican Xia

Publication date: 12 January 2024

zbMATH Keywords

local searchcylindrical algebraic decompositionSMTnonlinear real arithmeticcell-jump

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Local search for Boolean satisfiability with configuration checking and subscore
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Partial cylindrical algebraic decomposition for quantifier elimination
• raSAT: an SMT solver for polynomial constraints
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Constructing a single cell in cylindrical algebraic decomposition
• Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break
• Solving Non-linear Arithmetic
• A Model-Constructing Satisfiability Calculus
• Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
• Handbook of Model Checking
• Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• Computer Aided Verification
• The MathSAT5 SMT Solver
• Improved projection for cylindrical algebraic decomposition
• Local Search for SMT on Linear Integer Arithmetic

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