Local Search For Satisfiability Modulo Integer Arithmetic Theories

DOI10.1145/3597495MaRDI QIDQ6082229zbMATH OpenOpenAlexFDO

Authors Shaowei Cai, Bohan Li, X. D. 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

linear Integer arithmeticlocal searchnon-linear Integer arithmeticSMT

Mathematics Subject Classification ID

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

Abstract: Satisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a formula with respect to certain background first order theories. In this paper, we focus on Satisfiablity Modulo Integer Arithmetic, which is referred to as SMT(IA), including both linear and non-linear integer arithmetic theories. Dominant approaches to SMT rely on calling a CDCL-based SAT solver, either in a lazy or eager favor. Local search, a competitive approach to solving combinatorial problems including SAT, however, has not been well studied for SMT. We develop the first local search algorithm for SMT(IA) by directly operating on variables, breaking through the traditional framework. We propose a local search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for integer arithmetic, as well as a two-level operation selection heuristic. Putting these together, we develop a local search SMT(IA) solver called LS-IA. Experiments are carried out to evaluate LS-IA on benchmarks from SMTLIB. The results show that LS-IA is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets from SMT-LIB.

Cites work

• A constraint-based approach to solving games on infinite graphs
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• A model-constructing satisfiability calculus
• A practical approach to satisfiability modulo linear integer arithmetic
• CCAnr: a configuration checking based local search solver for non-random satisfiability
• Choosing probability distributions for stochastic local search and the role of make versus break
• Computer Aided Verification
• Computer Aided Verification
• Computing Stable Models via Reductions to Difference Logic
• Disequality management in integer difference logic via finite instantiations.
• Fast cube tests for LIA constraint solving
• Flexible proof production in an industrial-strength SMT solver
• Hilbert's Tenth Problem is Unsolvable
• scientific article; zbMATH DE number 1302201 (Why is no real title available?)
• scientific article; zbMATH DE number 1033831 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• scientific article; zbMATH DE number 1903355 (Why is no real title available?)
• scientific article; zbMATH DE number 956863 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Improving local search for random 3-SAT using quantitative configuration checking
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Lazy satisfiability modulo theories
• Local search for Boolean satisfiability with configuration checking and subscore
• Local Search for SMT on Linear Integer Arithmetic
• Local search with edge weighting and configuration checking heuristics for minimum vertex cover
• Model-driven visualizations of constraint-based local search
• Non-linear loop invariant generation using Gröbner bases
• Optimal speedup of Las Vegas algorithms
• Precise and complete propagation based local search for satisfiability modulo theories
• Propagation based local search for bit-precise reasoning
• Proving termination through conditional termination
• Real World Verification
• SAT modulo linear arithmetic for solving polynomial constraints
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Satisfiability modulo theories
• Solving nonlinear integer arithmetic with MCSAT
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• SPASS-SATT. A CDCL(LA) solver
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• Stochastic local search. Foundations and applications.
• Sums of three cubes
• The MathSAT5 SMT solver
• The small model property: How small can it be?
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(1)

• Boosting MCSat modulo nonlinear integer arithmetic via local search

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

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