27
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ community wiki? $\endgroup$ – Opt Aug 20 '10 at 3:42
  • $\begingroup$ I made this community wiki as per the suggestion. $\endgroup$ – Ross Snider Aug 20 '10 at 4:25
  • 1
    $\begingroup$ 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)? $\endgroup$ – MGwynne Nov 18 '11 at 15:01
21
$\begingroup$

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

$\endgroup$
  • $\begingroup$ This is a good example of an answer. It would be an even better answer if it were split into several. $\endgroup$ – Ross Snider Aug 20 '10 at 23:07
9
$\begingroup$

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.

$\endgroup$
8
$\begingroup$

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

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Ross Snider Jan 20 '12 at 18:45
7
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Particular hard instances (as opposed to instance families) are here satcompetition.org (See "benchmarks".) $\endgroup$ – Radu GRIGore Aug 20 '10 at 14:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.