Proving by Assignment Trees that
SAT Solvers are Non-Polynomial in
Unit Propagation Framework with 1 Selection and Cache
Gábor Kusper
gkusper@risc.uni-linz.ac.at
Research Institute for Symbolic Computation (RISC-Linz)
Johannes Kepler University, Linz, Austria
http://www.risc.uni-linz.ac.at/
October 23, 2003
Abstract
We introduce the Unit Propagation Framework with 1 Selection and Cache.
This framework is a SAT solver, which gets as a parameter a strategy
function, which tells us how to solve SAT. This framework is suitable to
simulate SAT solver algorithms, which use unit propagation to solve SAT
problems and the decision, which unit to propagate, is made about one
selected (usually a minimal) clause. SAT solvers may use cache, too. Any
such algorithm can be described by a strategy function. A strategy
function tells us which unit to propagate. We show that General
Unicorn-SAT (GUS), developed by the author, and the Davis, Putnam,
Logemann and Loveland procedure (DPLL) can be simulated in this framework
by giving the suitable strategy function. We show that DPLL and GUS use
the same number of unit propagations, 2^n + 2^(n-1) . 2, where n is the
number of variables, to show that CC, the set of all clear (full) clauses,
is unsatisfiable. Furthermore we introduce the Limitation Lemma, which
says that there is no SAT solver in this framework, which can show that CC
is unsatisfiable, using fewer unit propagations than DPLL. Hence, SAT
solvers are non-polynomial in this framework. To show this we use
assignment trees that are suitable to represent a run of this framework.