<p>The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (<a href="http://dx.doi.org/10.1016/j.jcss.2007.06.025">Journal</a>, <a href="http://eccc.hpi-web.de/eccc-reports/2002/TR02-035/index.html">ECCC</a>, <a href="http://www.lsi.upc.edu/~atserias/papers/width/submitted.pdf">author's copy</a>).</p>

<p>Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble game.
Recall that the existential pebble game is played between two competing players, called Spoiler and Duplicator, and the positions of the game are partial assignments of domain size at most $k+1$ to variables of $F$.
In the $(k+1)$-pebble game, starting from the empty assignment, Spoiler wants to falsify a clause from $F$ while remembering at most $k+1$ boolean values at a time, and Duplicator wants to prevent Spoiler from doing so.</p>

<p>The example is based on (the negation of) the pigeonhole principle.</p>

<blockquote>
  <p>For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{1, \dotsc, n \}$, let $p_{i,j}$ be a propositional variable meaning that pigeon $i$ sits in hole $j$.
  For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{0, \dotsc, n \}$, let $y_{i,j}$ be a new propositional variable.
  The following $3$-CNF formula ${EP}_i$ expresses that pigeon $i$ sits in some hole:
  $$ {EP}_i \equiv \neg y_{i,0} \wedge \bigwedge_{j=1}^n (y_{i,j-1} \vee p_{i,j} \vee \neg y_{i,j} ) \wedge y_{i,n}. $$
  Finally, the $3$-CNF formula ${EPHP}_n^{n+1}$ expressing the negation of the pigeonhole principle is the conjunction of all ${EP}_i$ and all clauses $H_k^{i,j} \equiv \neg p_{i,k} \vee \neg p_{j,k}$ for $i,j \in \{1, \dotsc, n+1 \}, i \ne j$ and $k \in \{1, \dotsc, n \}$.</p>
</blockquote>

<p>Lemma 6 of the paper gives a fairly short and intuitive proof that Spoiler cannot win the $n$-pebble game on ${EPHP}_n^{n+1}$, hence ${EPHP}_n^{n+1}$ has no resolution refutation of width at most $n-1$.</p>

<p>The paper has another example in Lemma 9, based on the dense linear order principle.</p>

<p>Given that computing the minimum width for resolution refutations is EXPTIME-complete, and moreover it takes $\Omega(n^{(k-3)/12})$ time to certify that the minimum width is at least $k+1$ (see Berkholz's paper in <a href="http://doi.ieeecomputersociety.org/10.1109/FOCS.2012.48">FOCS</a> or <a href="http://arxiv.org/abs/1204.0775">arXiv</a>), perhaps it is hard to come up with examples which provably need wide resolution refutations?</p>

CC BY-SA 3.0
2013-03-08T16:21:32.170Z
OK I should have known that. So $\mathrm{EPHP}^6_5$ (slightly simplified) would be an example that has 48 variables and about 100 clauses. If nothing significantly simpler comes up, I will accept this answer.
Jan Johannsen
CC BY-SA 3.0
2013-03-08T10:32:08.933Z
2013-03-09T21:23:39.657Z
2013-03-09T21:23:39.657Z
siuman
<p>Recall that the <em>width</em> of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring  in $R$. For every $w$, there are unsatisfiable formulas $F$ in 3-CNF s.t. every resolution refutation of $F$ requires width at least $w$. </p>

<p>I need a concrete example of an unsatisfiable formula in 3-CNF (as small and simple as possible) that has no resolution refutation of width 4. </p>

CC BY-SA 3.0
2013-03-07T17:03:13.813Z
Do you need exactly width 5 or at least width 5? In the latter case I guess few random clauses on an handful of variable will do. Not very nice and not very small, though.
MassimoLauria
CC BY-SA 3.0
2013-03-07T18:33:26.940Z
think relatively straightfwd computer/empirical search would find this or rule it out. also think there is some more general/interesting unexplored theory lurking here. see also [in resolution proofs, are all DAGs possible?](http://cstheory.stackexchange.com/questions/16500/in-sat-resolution-proofs-are-all-dags-possible), looking for reopen votes if you agree =) related question: for $m \times n$-SAT formulas, what dimension(s) resolution DAGs are possible?
vzn
CC BY-SA 3.0
2013-03-08T04:23:24.157Z
Jan, I think Jacob should be able to answer this easily. By the way, would you like to generalize the question a bit and ask about a method to come up with 3-CNFs of given resolution width?
Kaveh
CC BY-SA 3.0
2013-03-08T16:25:52.517Z
Massimo, I need a concrete example that I can actually write down and explain on a blackboard or so. So random clauses won't do.
Jan Johannsen
CC BY-SA 3.0
2013-03-12T20:24:56.933Z
I am in the the wrong time zone now to be able to think properly, but maybe a Tseitin formula over some really small graph (where you could check expansion by hand) would do? But you really need a 3-CNF, do you? For a 4-CNF I would perhaps play around with a rectangular grid of suitable dimensions and see what happens. Just some very half-baked thoughts...
Jakob Nordstrom
<cc.complexity-theory><lo.logic><sat><proof-complexity>
A 3-CNF formula that requires resolution width $5$
Jan Johannsen
# A 3-CNF formula that requires resolution width $5$

(Asked by: username_0 on 2013-03-07)

Recall that the *width* of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. For every $w$, there are unsatisfiable formulas $F$ in 3-CNF s.t. every resolution refutation of $F$ requires width at least $w$.

I need a concrete example of an unsatisfiable formula in 3-CNF (as small and simple as possible) that has no resolution refutation of width 4.

**Tags:** cc.complexity-theory, lo.logic, sat, proof-complexity

> **Comments:**
> **username_1**: Do you need exactly width 5 or at least width 5? In the latter case I guess few random clauses on an handful of variable will do. Not very nice and not very small, though.  
> **username_2**: think relatively straightfwd computer/empirical search would find this or rule it out. also think there is some more general/interesting unexplored theory lurking here. see also [in resolution proofs, are all DAGs possible?](http://cstheory.stackexchange.com/questions/16500/in-sat-resolution-proofs-are-all-dags-possible), looking for reopen votes if you agree =) related question: for $m \times n$-SAT formulas, what dimension(s) resolution DAGs are possible?  
> **username_3**: Jan, I think Jacob should be able to answer this easily. By the way, would you like to generalize the question a bit and ask about a method to come up with 3-CNFs of given resolution width?  
> **username_0**: Massimo, I need a concrete example that I can actually write down and explain on a blackboard or so. So random clauses won't do.  
> **username_4**: I am in the the wrong time zone now to be able to think properly, but maybe a Tseitin formula over some really small graph (where you could check expansion by hand) would do? But you really need a 3-CNF, do you? For a 4-CNF I would perhaps play around with a rectangular grid of suitable dimensions and see what happens. Just some very half-baked thoughts...  

---

## 1 answers

### Answer by username_5 on 2013-03-08. Score: 15 | Accepted answer

The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau ([Journal](http://dx.doi.org/10.1016/j.jcss.2007.06.025), [ECCC](http://eccc.hpi-web.de/eccc-reports/2002/TR02-035/index.html), [author's copy](http://www.lsi.upc.edu/~atserias/papers/width/submitted.pdf)).

Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble game.
Recall that the existential pebble game is played between two competing players, called Spoiler and Duplicator, and the positions of the game are partial assignments of domain size at most $k+1$ to variables of $F$.
In the $(k+1)$-pebble game, starting from the empty assignment, Spoiler wants to falsify a clause from $F$ while remembering at most $k+1$ boolean values at a time, and Duplicator wants to prevent Spoiler from doing so.

The example is based on (the negation of) the pigeonhole principle.

> For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{1, \dotsc, n \}$, let $p\_{i,j}$ be a propositional variable meaning that pigeon $i$ sits in hole $j$.
> For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{0, \dotsc, n \}$, let $y\_{i,j}$ be a new propositional variable.
> The following $3$-CNF formula ${EP}\_i$ expresses that pigeon $i$ sits in some hole:
> $$ {EP}\_i \equiv \neg y\_{i,0} \wedge \bigwedge\_{j=1}^n (y\_{i,j-1} \vee p\_{i,j} \vee \neg y\_{i,j} ) \wedge y\_{i,n}. $$
> Finally, the $3$-CNF formula ${EPHP}\_n^{n+1}$ expressing the negation of the pigeonhole principle is the conjunction of all ${EP}\_i$ and all clauses $H\_k^{i,j} \equiv \neg p\_{i,k} \vee \neg p\_{j,k}$ for $i,j \in \{1, \dotsc, n+1 \}, i \ne j$ and $k \in \{1, \dotsc, n \}$.

Lemma 6 of the paper gives a fairly short and intuitive proof that Spoiler cannot win the $n$-pebble game on ${EPHP}\_n^{n+1}$, hence ${EPHP}\_n^{n+1}$ has no resolution refutation of width at most $n-1$.

The paper has another example in Lemma 9, based on the dense linear order principle.

Given that computing the minimum width for resolution refutations is EXPTIME-complete, and moreover it takes $\Omega(n^{(k-3)/12})$ time to certify that the minimum width is at least $k+1$ (see Berkholz's paper in [FOCS](http://doi.ieeecomputersociety.org/10.1109/FOCS.2012.48) or [arXiv](http://arxiv.org/abs/1204.0775)), perhaps it is hard to come up with examples which provably need wide resolution refutations?

> **Comments:**
> **username_0**: OK I should have known that. So $\mathrm{EPHP}^6_5$ (slightly simplified) would be an example that has 48 variables and about 100 clauses. If nothing significantly simpler comes up, I will accept this answer.  

---

