(I posted this question on MathSE first, no answer, that is the reason why I come here.)

Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ are equivalent.

Question : Is it true that each 4-clause implied by $F$ (if there are any) is also the resolvent of two implied 3-clauses ? By extension, is it true that each $k$-clause ($k> 3$) implied by $F$ is also the resolvent of two strictly smaller implied clauses ? (a $k$-clause ($k\leq n$) contains exactly $k$ literals in it).

Thank you for your answers.

  • $\begingroup$ I think implication is better defined as $F \Rightarrow c$, which is the same as your definition. $\endgroup$ – Yuval Filmus Apr 9 '13 at 22:35

Here is a counterexample: $$ (a \lor y \lor s) \land (\overline{y} \lor b \lor z) \land (\overline{z} \lor c \lor d) \land (\overline{s} \lor b \lor t) \land (\overline{t} \lor c \lor d). $$ This formula implies $a \lor b \lor c \lor d$, but only the five listed 3-clauses, no two of which resolve to $a\lor b\lor c\lor d$.

| cite | improve this answer | |
  • 1
    $\begingroup$ I verified that only these 3-clauses are implied using a computer program. $\endgroup$ – Yuval Filmus Apr 10 '13 at 0:13
  • $\begingroup$ Perfect counterexample, tks ! The structure of such formula seems very tight, I'll deepen it. $\endgroup$ – Xavier Labouze Apr 10 '13 at 6:01
  • 1
    $\begingroup$ Here is the shortest counterexample : $(x \lor y \lor a) \land (\overline{x} \lor b \lor c) \land (\overline{y} \lor b\lor d)$ implying $(a \lor b \lor c\lor d)$ $\endgroup$ – Xavier Labouze Jul 20 '13 at 13:50

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.