Local Search For Satisfiability Modulo Integer Arithmetic Theories

TL;DR

This paper introduces LS-IA, the first local search algorithm for SMT with integer arithmetic, which operates directly on variables and shows competitive performance on SMTLIB benchmarks.

Contribution

The paper presents a novel local search framework for SMT(IA), including new operators and heuristics, breaking traditional reliance on CDCL-based solvers.

Findings

LS-IA is competitive with state-of-the-art SMT solvers.

Performs especially well on formulas with only integer variables.

A portfolio with Z3 improves the state-of-the-art on satisfiable benchmarks.

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.