<p>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$.</p>

CC BY-SA 3.0
2013-04-10T00:13:03.090Z
I verified that only these 3-clauses are implied using a computer program.
Yuval Filmus
CC BY-SA 3.0
2013-04-10T06:01:10.987Z
Perfect counterexample, tks ! The structure of such formula seems very tight, I'll deepen it.
Xavier Labouze
CC BY-SA 3.0
2013-07-20T13:50:21.347Z
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
CC BY-SA 3.0
2013-04-09T23:23:15.263Z
2013-04-09T23:23:15.263Z
Yuval Filmus
<p>(I posted this question on MathSE first, no answer, that is the reason why I come here.)</p>

<p>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. </p>

<p><strong>Question</strong> : 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&gt; 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).</p>

<p>Thank you for your answers. </p>

CC BY-SA 3.0
2013-04-09T22:35:18.523Z
I think implication is better defined as $F \Rightarrow c$, which is the same as your definition.
Yuval Filmus
<cc.complexity-theory><lo.logic><sat><resolution>
Implied Clause and Resolvent
Xavier Labouze
# Implied Clause and Resolvent

(Asked by: username_0 on 2013-04-09)

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

**Tags:** cc.complexity-theory, lo.logic, sat, resolution
> **Comments:**
> **username_1**: I think implication is better defined as $F \Rightarrow c$, which is the same as your definition.  

---

## 1 answers

### Answer by username_1 on 2013-04-09. Score: 9 | Accepted answer

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$.

> **Comments:**
> **username_1**: I verified that only these 3-clauses are implied using a computer program.  
> **username_0**: Perfect counterexample, tks ! The structure of such formula seems very tight, I'll deepen it.  
> **username_0**: 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)$  

---

