Well known classes of boolean formulas that require exponentially long resolution proofs

Question

You might often find cutting plane methods, variable propagation, branch and bound, clause learning, intelligent backtracking or even handwoven human heuristics in SAT solvers. Yet for decades the best SAT solvers have relied heavily on resolution proof techniques and use a combination of other things simply for aid and to direct resolution-style search. Obviously, it's suspected that ANY algorithm will fail to decide the satisfiability question in polynomial time in at least some cases.

In 1985, Haken proved in his paper "The intractability of resolution" that the pigeon hole principle encoded in CNF does not admit polynomial sized resolution proofs. While this does prove something about the intractability of resolution-based algorithms, it also gives criteria by which cutting edge solvers can be judged - and in fact one of the many considerations that goes into designing a SAT solver today is how it is likely to perform on known 'hard' cases.

Having a list of classes of Boolean formulas that provably admit exponentially sized resolution proofs is useful in the sense it gives 'hard' formulas to test new SAT solvers against. What work has been done in compiling such classes together? Does anyone have a reference containing such a list and their relevant proofs? Please list one class of Boolean formula per answer.

Answer 1

Hard instances for resolution:

1. Tseitin's formulas (over expander graphs).

2. Weak ($ m $ to $ n$) pigeonhole principle (exponential in $n$ lower bounds, for any $ m>n $).

3. Random 3CNF's with $ n $ variables and $ O(n^{1.5-\epsilon})$ clauses, for $ 0<\epsilon<1/2 $.

Good, relatively up-to-date, technical survey for proof complexity lower bounds, see:

Nathan Segerlind: The Complexity of Propositional Proofs. Bulletin of Symbolic Logic 13(4): 417-481 (2007) available at: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Answer 2

There are a number of good surveys and books on propositional proof complexity which contain such lists. Many proof systems p-simulate resolution, therefore any formula which is hard for them will be hard for resolution.

Books:
1. Jan Krajicek, "Bounded arithmetic, propositional logic, and complexity theory", 1995
2. Stephen A. Cook and Phoung The Neguyen, "Logical Foundations of Proof Complexity", 2010

Surveys:
1. Paul Beame, and Toniann Pitassi, "Propositional proof complexity: Past, Present and Future", 2001
2. Samuel R. Buss, "Bounded Arithmetic and Propositional Proof Complexity", 1997
3. Alasdair Urquhart, "The complexity of propositional proofs", 1995

Also see those listed here and here.

Answer 3

Another hard example for resolution is the mutilated chessboard formulas. They state that a $2n \times 2n$ chessboard with two diagonally opposite corners missing cannot be covered with $2\times 1$ tiles. See:

Michael Alekhnovich. Mutilated chessboard problem is exponentially hard for resolution. Theoretical Compututer Science 310(1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

Answer 4

Pavel Pudlák has recently shown an exponential lower bound for Resolution refutations of the formulas derived from the Ramsey theorem $n\to (k)^2_2$ for $k=\lfloor \frac12 \log n \rfloor$. These formulas have clauses $\bigvee_{i,j\in K} x_{i,j}$ and $\bigvee_{i,j\in K} \neg x_{i,j}$ for every subset $K\subseteq \{ 1 , \ldots , n \}$ of size $|K| = k$, they are unsatisfiable due to the Ramsey theorem. This lower bound was a long-standing open problem, the proof is published in this ECCC-report.

Answer 5

There is a construction on page 9 of this paper by Groote and Zantema.

Answer 6

Doesn't DIMACS maintain sample sets of hard SAT instances? I couldn't find it there with just a cursory look, but if you enter "SAT" into their search box it will bring up many hits including several papers/talks on hard SAT instances.