Local Search For SMT On Linear and Multilinear Real Arithmetic

Satisfiability Modulo Theories (SMT) has significant application in various domains. In this paper, we focus on 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 fragment where the atomic constraints are multilinear. We proposed the first local search algorithm for SMT(RA), called LS-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 LS-RA on benchmarks from SMT-LIB. The results show that LS-RA is competitive with the state-of-the-art SMT solvers, and performs particularly well on multilinear instances.