4
$\begingroup$

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 ?

$\endgroup$
10
$\begingroup$

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\})$.

$\endgroup$
  • $\begingroup$ Very short, very clear, thank you very much ! $\endgroup$ – Xavier Labouze Mar 11 '13 at 15:35

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.