13
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – MassimoLauria Mar 7 '13 at 17:03
  • 1
    $\begingroup$ 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?, looking for reopen votes if you agree =) related question: for $m \times n$-SAT formulas, what dimension(s) resolution DAGs are possible? $\endgroup$ – vzn Mar 7 '13 at 18:33
  • $\begingroup$ 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? $\endgroup$ – Kaveh Mar 8 '13 at 4:23
  • $\begingroup$ 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. $\endgroup$ – Jan Johannsen Mar 8 '13 at 16:25
  • 1
    $\begingroup$ 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... $\endgroup$ – Jakob Nordstrom Mar 12 '13 at 20:24
14
$\begingroup$

The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (Journal, ECCC, author's copy).

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 or arXiv), perhaps it is hard to come up with examples which provably need wide resolution refutations?

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Jan Johannsen Mar 8 '13 at 16:21

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.