<p>Sure. If $C_1\ni x_i$ and $C_2\ni\neg x_i$ are in $F\restriction I$ (in particular, $x_i$ is unset by $I$), pick clauses $D_1,D_2$ in $F$ which restrict to $C_1$ and $C_2$, respectively. Then $x_i\in D_1$ and $\neg x_i\in D_2$, hence their resolvent $(D_1\let\bez\smallsetminus\bez\{x_i\})\cup(D_2\bez\{\neg x_i\})$ is subsumed by some $D\in F$. If $D$ contains a literal made true under $I$, then so does $D_1$ or $D_2$, contradicting their choice. Thus, $D\restriction I$ is in $F\restriction I$, and it subsumes $(C_1\bez\{x_i\})\cup(C_2\cup\{\neg x_i\})$.</p>

CC BY-SA 3.0
2013-03-11T15:35:02.760Z
Very short, very clear, thank you very much !
Xavier Labouze
CC BY-SA 3.0
2013-03-11T15:21:36.557Z
2013-03-11T15:21:36.557Z
Emil Jeřábek
<p>The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. Thank you for your attention. </p>

<p>A CNF formula is closed under resolution if all the possible resolvents are subsumed by a clause of the formula - a clause $c_1$ is subsumed by a clause $c_2$ if all the literals of $c_2$ are in $c_1$ (any clause is subsumed by itself then).</p>

<p>Given $F$,  a 3-CNF formula on $n$ variables $(x_i)$$_{i\le 1 \le n}$ which is closed under resolution. Given $I$, a partial assignment of $k$ variables among $(x_i)\   (k\le n)$. Let $F_{|I}$ the induced formula by applying $I$ to $F$: Any clause that contains a literal which evaluates to "true" under $I$ is deleted from the formula and any literals that evaluate to "false" under $I$ are deleted from all clauses -  the clauses that become empty by this deletion remain in the formula as the empty clause.</p>

<p><strong>Question</strong>: Is $F_{|I}$ closed under resolution ?</p>

<cc.complexity-theory><lo.logic><sat><boolean-functions><resolution>
About Closure under Resolution
Xavier Labouze
# About Closure under Resolution

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

The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. Thank you for your attention.

A CNF formula is closed under resolution if all the possible resolvents are subsumed by a clause of the formula - a clause $c\_1$ is subsumed by a clause $c\_2$ if all the literals of $c\_2$ are in $c\_1$ (any clause is subsumed by itself then).

Given $F$, a 3-CNF formula on $n$ variables $(x\_i)$$\_{i\le 1 \le n}$ which is closed under resolution. Given $I$, a partial assignment of $k$ variables among $(x\_i)\ (k\le n)$. Let $F\_{|I}$ the induced formula by applying $I$ to $F$: Any clause that contains a literal which evaluates to "true" under $I$ is deleted from the formula and any literals that evaluate to "false" under $I$ are deleted from all clauses - the clauses that become empty by this deletion remain in the formula as the empty clause.

**Question**: Is $F\_{|I}$ closed under resolution ?

**Tags:** cc.complexity-theory, lo.logic, sat, boolean-functions, resolution

---

## 1 answers

### Answer by username_1 on 2013-03-11. Score: 10 | Accepted answer

Sure. If $C\_1\ni x\_i$ and $C\_2\ni\neg x\_i$ are in $F\restriction I$ (in particular, $x\_i$ is unset by $I$), pick clauses $D\_1,D\_2$ in $F$ which restrict to $C\_1$ and $C\_2$, respectively. Then $x\_i\in D\_1$ and $\neg x\_i\in D\_2$, hence their resolvent $(D\_1\let\bez\smallsetminus\bez\{x\_i\})\cup(D\_2\bez\{\neg x\_i\})$ is subsumed by some $D\in F$. If $D$ contains a literal made true under $I$, then so does $D\_1$ or $D\_2$, contradicting their choice. Thus, $D\restriction I$ is in $F\restriction I$, and it subsumes $(C\_1\bez\{x\_i\})\cup(C\_2\cup\{\neg x\_i\})$.

> **Comments:**
> **username_0**: Very short, very clear, thank you very much !  

---

