Local Search For SMT On Linear and Multilinear Real Arithmetic
Bohan Li, Shaowei Cai

TL;DR
This paper introduces LocalSMT(RA), the first local search algorithm for SMT over real arithmetic, which effectively handles linear and multi-linear cases by using interval-based operators and tie-breaking mechanisms, showing competitive results.
Contribution
The paper presents the first local search approach for SMT(RA), incorporating interval-based operators and tie-breaking strategies to improve performance on multi-linear instances.
Findings
LocalSMT(RA) is competitive with state-of-the-art SMT solvers.
The algorithm performs particularly well on multi-linear real arithmetic instances.
Experimental results validate the effectiveness of the proposed methods.
Abstract
Satisfiability Modulo Theories (SMT) has significant application in various domains. In this paper, we focus on quantifier-free Satisfiablity Modulo Real Arithmetic, referred to as SMT(RA), including both linear and non-linear real arithmetic theories. As for non-linear real arithmetic theory, we focus on one of its important fragments where the atomic constraints are multi-linear. We propose the first local search algorithm for SMT(RA), called LocalSMT(RA), based on two novel ideas. First, an interval-based operator is proposed to cooperate with the traditional local search operator by considering the interval information. Moreover, we propose a tie-breaking mechanism to further evaluate the operations when the operations are indistinguishable according to the score function. Experiments are conducted to evaluate LocalSMT(RA) on benchmarks from SMT-LIB. The results show that…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Constraint Satisfaction and Optimization
