# Implied Clause and Resolvent

(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).

• I think implication is better defined as $F \Rightarrow c$, which is the same as your definition. – 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$.
• 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)$ – Xavier Labouze Jul 20 '13 at 13:50