An Evolutionary Local Search Method for Incremental Satisfiability - Artificial Intelligence and Symbolic Computation - page 143

An Evolutionary Local Search Method
for Incremental Satisfiability

Mohamed El Bachir Menaï

Artificial Intelligence Laboratory, University of Paris 8
2 rue de la liberté, 93526 Saint Denis, France
[e-mail]

Abstract. Incremental satisfiability problem (ISAT) is considered as a generali-
sation 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 pa-
rameter and had proved competitive with the more elaborate stochastic local
search methods on many hard optimization problems such as MAXSAT prob-
lem. 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.
Keywords: Incremental Satisfiability, Stochastic Local Search, Extremal Op-
timization, Self-Organized Criticality

1 Introduction

The Boolean satisfiability problem (SAT) is one of the most important discrete con-
straint satisfaction problems. It is defined as follows. Let Bool denotes the Boolean
domain

{} { }

0 and X = x , 2 x ,...,

x

be a set of Boolean variables. The set of literals

1

{ }

over X is /, . A clause C on X is a disjunction of literals. A SAT

instance is a conjunction of clauses. An assignment of n Boolean variables is a sub-
stitution of these variables by a vector

L = x x x ∈ X

n

. A literal x or x is said to be satis-
fiable by an assignment if its variable is mapped to 1 or 0, respectively. A clause C is
said to be satisfiable by an assignment v if at least one of its literals is satisfiable by v ,
in such case the value of the clause equals 1 (

v ∈ Bool

() C v = 1

), otherwise it is said to be

()

vC ). A model for a SAT is an assignment where all clauses are
satisfiable. The SAT problem asks to find a model for a given set of clauses.
SAT is a paradigmatic NP -complete problem in logic and computing theory [9]. It
provides a natural mathematical formalism to encode information about many prob-

= 0

unsatisfiable (