Local Search For Satisfiability Modulo Integer Arithmetic Theories

DOI10.1145/3597495arXiv2211.10219OpenAlexW4377021963MaRDI QIDQ6082229

Bohan Li, Shaowei Cai, Xindi Zhang

Publication date: 3 November 2023

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2211.10219

zbMATH Keywords

local searchSMTlinear Integer arithmeticnon-linear Integer arithmetic

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SAT modulo linear arithmetic for solving polynomial constraints
• Local search for Boolean satisfiability with configuration checking and subscore
• Local search with edge weighting and configuration checking heuristics for minimum vertex cover
• Optimal speedup of Las Vegas algorithms
• Propagation based local search for bit-precise reasoning
• The small model property: How small can it be?
• Flexible proof production in an industrial-strength SMT solver
• Model-driven visualizations of constraint-based local search
• SPASS-SATT. A CDCL(LA) solver
• Fast Cube Tests for LIA Constraint Solving
• A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
• Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break
• A Model-Constructing Satisfiability Calculus
• Solving Nonlinear Integer Arithmetic with MCSAT
• Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
• Satisfiability Modulo Theories
• Proving Termination Through Conditional Termination
• Non-linear loop invariant generation using Gröbner bases
• CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
• Solving SAT and SAT Modulo Theories
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Computing Stable Models via Reductions to Difference Logic
• Hilbert's Tenth Problem is Unsolvable
• Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
• Sums of three cubes
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
• Real World Verification
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• The MathSAT5 SMT Solver
• A constraint-based approach to solving games on infinite graphs
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Local Search For Satisfiability Modulo Integer Arithmetic Theories