<p>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.</p>

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

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

<p>Also see those listed <a href="http://www.karlin.mff.cuni.cz/~krajicek/syll10.html">here</a> and <a href="http://en.wikipedia.org/wiki/Proof_complexity">here</a>.</p>

CC BY-SA 2.5
2010-08-20T09:51:52.207Z
2010-08-21T05:36:04.207Z
2010-08-21T05:36:04.207Z
Kaveh
<p>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:</p>

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

CC BY-SA 3.0
2011-11-18T09:48:54.893Z
2011-11-18T09:48:54.893Z
Jan Johannsen
<p>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 <a href="http://eccc.hpi-web.de/report/2011/162/">ECCC-report</a>. </p>

CC BY-SA 3.0
2012-01-20T18:45:17.720Z
Thanks. This is a very interesting answer (although the notation is a bit different I could follow). My undergrad advisor studied Ramsey Theory extensively. He was successful in installing that interest in me as well.
Ross Snider
CC BY-SA 3.0
2012-01-20T12:42:33.560Z
2012-01-20T12:42:33.560Z
Jan Johannsen
<p>There is a construction on page 9 of this <a href="http://scholar.google.com/scholar?hl=en&amp;q=Resolution+and+binary+decision+diagrams+cannot+simulate+each+other+polynomially" rel="nofollow">paper by Groote and Zantema</a>.</p>

CC BY-SA 3.0
2010-08-20T06:41:50.237Z
2011-11-18T17:03:34.597Z
2011-11-18T17:03:34.597Z
Radu GRIGore
<p>Doesn't <a href="http://dimacs.rutgers.edu/" rel="nofollow">DIMACS</a> 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.</p>

CC BY-SA 2.5
2010-08-20T14:02:25.683Z
Particular hard instances (as opposed to instance families) are here http://www.satcompetition.org/ (See "benchmarks".)
Radu GRIGore
CC BY-SA 2.5
2010-08-20T13:40:30.450Z
2010-08-20T13:40:30.450Z
Kurt
<p><strong>Hard instances for resolution</strong>:</p>

<ol>
<li><p>Tseitin's formulas (over expander graphs).</p></li>
<li><p>Weak ($ m $ to $ n$) pigeonhole principle (exponential in $n$ lower bounds, for any $ m>n $).</p></li>
<li><p>Random 3CNF's with $ n $ variables and $ O(n^{1.5-\epsilon})$ clauses, for $ 0&lt;\epsilon&lt;1/2 $.</p></li>
</ol>

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

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

CC BY-SA 2.5
2010-08-20T23:07:49.730Z
This is a good example of an answer. It would be an even better answer if it were split into several.
Ross Snider
CC BY-SA 2.5
2010-08-20T11:57:22.083Z
2010-08-20T12:59:38.723Z
2010-08-20T12:59:38.723Z
Iddo Tzameret
<p>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.</p>

<p>In 1985, Haken proved in his paper <a href="http://www.sciencedirect.com/science?_ob=ArticleURL&amp;_udi=B6V1G-48HRYBH-P&amp;_user=10&amp;_coverDate=12%2F31%2F1985&amp;_rdoc=1&amp;_fmt=high&amp;_orig=search&amp;_sort=d&amp;_docanchor=&amp;view=c&amp;_searchStrId=1436167533&amp;_rerunOrigin=scholar.google&amp;_acct=C000050221&amp;_version=1&amp;_urlVersion=0&amp;_userid=10&amp;md5=3eadc0120fda0dd052d1f9a8007b9f66">"The intractability of resolution"</a> 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.</p>

<p>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.</p>

CC BY-SA 3.0
2011-11-18T15:01:59.763Z
An additional aspect to this question that I'd be interested in: are there *explicit* known poly-size proofs for extended-resolution for these hard cases (like Cook's proof of weak pigeon-hole formulas)?
MGwynne
CC BY-SA 2.5
2010-08-20T03:42:07.517Z
community wiki?
Opt
CC BY-SA 2.5
2010-08-20T04:25:48.707Z
I made this community wiki as per the suggestion.
Ross Snider
<reference-request><big-list><sat><proof-complexity><lo.logic>
Well known classes of boolean formulas that require exponentially long resolution proofs
Ross Snider
# Well known classes of boolean formulas that require exponentially long resolution proofs

(Asked by: username_0 on 2010-08-20)

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"](http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1G-48HRYBH-P&_user=10&_coverDate=12%2F31%2F1985&_rdoc=1&_fmt=high&_orig=search&_sort=d&_docanchor=&view=c&_searchStrId=1436167533&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=3eadc0120fda0dd052d1f9a8007b9f66) 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.

**Tags:** reference-request, big-list, sat, proof-complexity, lo.logic

> **Comments:**
> **username_2**: community wiki?  
> **username_0**: I made this community wiki as per the suggestion.  
> **username_1**: An additional aspect to this question that I'd be interested in: are there *explicit* known poly-size proofs for extended-resolution for these hard cases (like Cook's proof of weak pigeon-hole formulas)?  

---

## 6 answers

### Answer by username_7 on 2010-08-20. Score: 22 | Accepted answer

**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>

> **Comments:**
> **username_0**: This is a good example of an answer. It would be an even better answer if it were split into several.  

---

### Answer by username_3 on 2010-08-20. Score: 9

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](http://www.karlin.mff.cuni.cz/~krajicek/syll10.html) and [here](http://en.wikipedia.org/wiki/Proof_complexity).


---

### Answer by username_4 on 2011-11-18. Score: 9

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 by username_4 on 2012-01-20. Score: 8

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](http://eccc.hpi-web.de/report/2011/162/).

> **Comments:**
> **username_0**: Thanks. This is a very interesting answer (although the notation is a bit different I could follow). My undergrad advisor studied Ramsey Theory extensively. He was successful in installing that interest in me as well.  

---

### Answer by username_5 on 2010-08-20. Score: 7

There is a construction on page 9 of this [paper by Groote and Zantema](http://scholar.google.com/scholar?hl=en&q=Resolution+and+binary+decision+diagrams+cannot+simulate+each+other+polynomially).


---

### Answer by username_6 on 2010-08-20. Score: 1

Doesn't [DIMACS](http://dimacs.rutgers.edu/) 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.

> **Comments:**
> **username_5**: Particular hard instances (as opposed to instance families) are here http://www.satcompetition.org/ (See "benchmarks".)  

---

