How to prove that the following simplification rule on Davis–Putnam function is satisfiability-equivalent?

Question

Denote $F\stackrel{\text{SAT}}{\equiv}H$ if $F \in SAT {\iff} H \in SAT$.

A transformation of formulas $S(·)$ is called satisfiability-equivalent if $\forall{F}\space F\stackrel{\text{SAT}}{\equiv}S(F)$.

How to prove that the following simplification rule is satisfiability-equivalent and show how to re-construct a satisfying assignment for the original formula $F$ from a satisfying assignment for the simplified formula: ${DP}_x(F)$ (the rule transforms F into ${DP}_x(F)$.

Note:- ${DP}_x(F)$ is the Davis–Putnam formula. The Davis–Putnam procedure eliminates variables one by one using the following function:

Function ${DP}_x(F)$ (// simplifies $F$ by getting rid of $x$ )

1. Add all resolvents by $x$ to $F$.
2. Remove all clauses containing $x$ or $\bar{x}$.

Answer 1

The DP algorithm can be described as follows.

Select a literal $l_i$ (a variable or the complement of a variable) and apply the algorithm recursively to search for a satisfying assignment for the formula $F[l_i \leftarrow \bot]$, i.e. the formula obtaind assigning False to literal $l_i$.

If the search succeeds, then we have a satisfying assignment for $F$. Otherwise, repeat the search with the formula $F[l_i \leftarrow \top]$.

If neither of these searches finds a satisfying assignment, then $F$ is unsatisfiable.

The procedure is based on the resolution rule saying that if $C_1$ and $C_2$ are clauses containing two complemantry literal $x$ and $\lnot x$ i.e. $C_1$ is $D_1 \lor x$ and $C_2$ is $D_2 \lor \lnot x$, then any assignment that satisfies both clauses $C_1$ and $C_2$ also satisfies $D_1 \lor D_2$. The clause $D_1 \lor D_2$ is said to be a resolvent of the original clauses (called parent clauses) on the variable $x$.

If we agree on this, we have to show that to resolve a pair of clauses with complementary literals $x$ and $\lnot x$ (step 1) preserves satisfiability: see below.

Regarding step 2, a "tautological" clause $x \lor ¬x$ is always satisfiable (it is equivalent to $\top$); thus every clause containing a "tautological" part has form $\alpha \lor \top$ and can be removed because it is satisfiable.

---

Now for the proof of the main result:

(i) Let $C_1$ and $C_2$ be satisfiable under an interpretation I. Since $x$ and $\lnot x$ are complementary, either $I(x) = \top$ or $I(\lnot x) = \top$. Suppose that $I(x) = \top$; then $I(\lnot x) = \bot$ and $C_2 = D_2 \lor \lnot x$ can be satisfied only if $I(D_2) = \top$.

But the resolvent $C$ is $D_1 \lor D_2$, and thus $I$ is also a model of it. A symmetric argument holds if $I(\lnot x) = \top$.

(ii) Conversely, let $I$ be an interpretation which satisfies $C$; then $I(l) = \top$ for at least one literal $l$ occurring in $C$.

By the resolution rule, either $l$ occurs in $C_1$ or $l$ occurs in $C_2$ (or both). In the first case we have $I(C_1) = \top$. Since neither $x$ nor $\lnot x$ occur in the resolvent $C$, the (partial) interpretation $I$ is not defined on them, and we can extend it to an "larger" one $I'$ defining $I'(\lnot x) = \top$.

Since $C_2$ is $D_2 \lor \lnot x$, we have $I'(C_2) = \top$ and $I'(C_1) = I(C_1) = \top$; so $I'$ is a model for both $C_1$ and $C_2$. A symmetric argument holds if $l$ occurs in $C_2$.

Conclusion: let $F$ the formula and let $H$ the "transformed" one. Starting from $I$ such that $I(H)=\top$, and thus $I$ satisfies the resolvent $C$, we define $I'$ that is equal to $I$ plus the condition that $I'(\lnot x)= \top$ or not according to the way that $I$ satisfies the resolvent clause.