An Evolutionary Local Search Method for Incremental Satisfiability

Abstract

Incremental satisfiability problem (ISAT) is considered as a generalisation of the Boolean satisfiability problem (SAT). It involves checking whether satisfiability is maintained when new clauses are added to an initial satisfiable set of clauses. Since stochastic local search algorithms have been proved highly efficient for SAT, it is valuable to investigate their application to solve ISAT. Extremal Optimization is a simple heuristic local search method inspired by the dynamics of living systems with evolving complexity and their tendency to self-organize to reach optimal adaptation. It has only one free parameter and had proved competitive with the more elaborate stochastic local search methods on many hard optimization problems such as MAXSAT problem. In this paper, we propose a novel Extremal Optimization based method for solving ISAT. We provide experimental results on ISAT instances and compare them against the results of conventional SAT algorithm. The promising results obtained indicate the suitability of this method for ISAT. © Springer-Verlag 2004.