A Tutorial on Time and Space Bounds in Tree-Like Resolution

摘要

Tree-like resolution is a well-known method for proving the unsatisfiability of a given formula. Lower bounds for the size and space in treelike 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.