This preprint was accepted December 14, 2001
Contact:
E. Hirsch
ABSTRACT:
In this paper we present a new randomized algorithm for SAT, i.e.,
the satisfiability problem
for Boolean formulas in conjunctive normal form.
Despite its simplicity,
this algorithm performs well on many common benchmarks
ranging from graph coloring problems to microprocessor verification.
For instance, compared to other
contemporary incomplete SAT solvers, it
dominates on satisfiable instances of
``{\tt aim}'' \cite{AIM96},
``{\tt ssa}'' \cite{L92},
``{\tt par}'' \cite{DIMACS} and
``{\tt ii}'' \cite{KKRR92} series.
It is also able to solve some of
the ``{\tt qg}'' \cite{ZH94} instances,
all satisfiable Velev's microprocessor verification instances
from series
``{\tt SSS.1.0}'' \cite{Vel:SSS.1.0},
``{\tt SSS.1.0a}'' \cite{Vel:SSS.1.0a} and
``{\tt SSS-SAT.1.0}'' \cite{Vel:SSS-SAT.1.0},
and most instances from ``{\tt VLIW-SAT.1.1}'' \cite{Vel:VLIW-SAT.1.1}.
Our algorithm is inspired by two randomized algorithms having
the best current worst-case upper bounds
(\cite{PPSZ98,PPZ97} and \cite{Sch99,SSW01}).
In our paper we combine the main ideas of these algorithms
in one algorithm.
The two approaches we use are local search
(which is used in many SAT algorithms, e.g., in GSAT \cite{SLM92} and
WalkSAT \cite{SKC94})
and unit clause elimination (which is rarely used
in local search algorithms).
In this paper we do not prove any theoretical bounds.
However, we present encouraging results of first computational experiments.
We also prove that our algorithm is probabilistically
approximately complete (PAC).
[Full text:
(.ps.gz)]