Information Technology Reference
In-Depth Information
Chapter 9
A Tutorial on Time and Space Bounds
in Tree-Like Resolution
Jacobo Torán
Abstract
Tree-like resolution is a well-known method for proving the
unsatisfiability of a given formula. Lower bounds for the size and space in tree-
like resolution imply lower bounds for many of the algorithms used in practice to
solve satisfiability problems. We review a combinatorial game that can be used to
prove lower and upper bounds for size and space in tree-like resolution and show
some of its applications.
·
Keywords
Resolution
Combinatorial games
9.1 Introduction
Let us first introduce some notation needed to understand the tutorial. The Boolean
formulas considered here are in conjunctive normal form (CNF), that is, they are
a conjunction of clauses. A clause is a disjunction of literals (variables or negated
variables). We will also talk about a set of clauses to refer to a formula. An assignment
ˇ
for a formula
F
is (partial) mapping from the set of variables in the formula to
{
0
,
1
}
. We denote by
F
ˇ
the result of substituting in
F
the variables assigned by
ˇ
by the corresponding value and reducing the formula in the intuitive way. If
F
ˇ
is
1 then we say that
is a satisfying assignment for
F
. If some satisfying assignment
for
F
exists, then we say that
F
is satisfiable, otherwise it is unsatisfiable.
Robinson introduced in [
Rob65
] the concept of
resolution
, a method for deciding
if a given formula in conjunctive normal form is unsatisfiable. Due to its simplicity
and to its importance in automatic theorem proving and logic programming systems,
resolution is one of the best studied refutation systems. The only inference rule in
this proof system is the resolution rule:
ˇ
