How to prove that the following simplification rule is satisfiability-equivalent?

361 Views Asked by At

Denote $F\overset{\text{SAT}}{\equiv}G$ if $F \in SAT {\iff} G \in SAT$.

A transformation of formulas $S(·)$ is called satisfiability-equivalent if $\forall{F}\space F\overset{\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: Blocked clause removal (the rule removes a blocked clause from $F$).

N.B.- Blocked clause: A literal $\ell$ in a clause $C$ blocks it if $\forall{D}\in F (\bar\ell \in D \implies |C \cap \overline{D}| \geq 2)$, that is, if $\bar\ell\in D$, then $C$ and $D$ must also have at least one other pair of contrary literals.

1

There are 1 best solutions below

0
On

Since OP said, they don't know how to start, I will try to provide an outline for a possible proof:

What do we have to prove?

The stated claim is that deleting a blocked clause from a SAT-formula does not change its satisfiability. So, let $F$ be some SAT-formula with a blocked clause $C$ (blocked by a literal $\ell \in C$) and let $G$ be the SAT-formula obtained from $F$ by deleting $C$. We then have to show that $F$ has a satisfying assignment if and only if $G$ has a satisfying assignment. Thus, we have to show two implications:

  1. $F$ satisfiable $\implies G$ satisfiable
  2. $G$ satisfiable $\implies F$ satisfiable

The trivial direction (1.)

Since deleting a clause only makes it easier to satisfy a SAT-formula, the first implication is trivial. To double check whether this is really clear: How can you get a satisfying assignment of $G$ from one of $F$?

The interesting directions (2.)

Here, we can assume that we have some satisfying assignment $\beta$ for $G$. If this assignment also satisfies $F$, we are done. So, it suffices to consider the case where the assignment $\beta$ does not satisfy $F$.

As $F$ and $G$ only differ in the clause $C$, this must mean that $\beta$ does not satisfy this clause $C$ (i.e. sets all literals in $C$ to False). Our goal, therefore, must be to somehow change $\beta$ such that it also satisfies $C$ while still satisfying all other clauses.

Now, how can we make sure that $C$ is satisfied? We have to set one of the literals in $C$ to True. But there is only one literal we know to be in $C$: The literal $\ell$! So, let's try setting this literal to True (while keeping all other assignments as in $\beta$:

This certainly satisfies $C$. And what about the other clauses? To check that those are still satisfied, take any such clause $D \neq C$ and consider the following three cases:

  1. $D$ contains neither $\ell$ nor $\bar \ell$
  2. $D$ contains $\ell$
  3. $D$ contains $\bar\ell$

We have to show that $D$ is satisfied by the new assignment in all three cases. Case 1 and 2 are easy (why?), in case 3 we should probably use the definition of a blocked clause (since we haven't used it yet) together with our assumption that $C$ wasn't satisfied by the original assignment $\beta$.