Stochastic local search for incremental SAT

Abstract

The boolean satisfiability problem (SAT) is stated as follows: given a boolean formula in CNF, find a truth assignment that satisfies its clauses. In this paper, we present a general framework based on stochastic local search and the structure of the CNF formula for solving incremental SAT problems. Given a satisfiable boolean formula in CNF, incremental SAT consists of checking whether the satisfiability is preserved when new clauses are added to the current clause set and if not, look for a new assignment that satisfies the old clauses and the new ones. The results of the experimentation we have conducted demonstrate the efficiency of our method to deal with large randomly generated incremental SAT problems.