Section 7.2.2.2: Satisfiability

Exercise 383. ▶ [23] [23] (Inprocessing.) A SAT solver can partition its database of current clauses into two parts, the "hard" clauses $\Phi$ and the "soft" clauses $\Psi$. Initially $\Psi$ is empty, while $\Phi$ is $F$, the set of all input clauses. Four kinds of changes are subsequently allowed:

• Learning. We can append a new soft clause $C$, provided that $\Phi \cup \Psi \cup C$ is satisfiable whenever $\Phi \cup \Psi$ is satisfiable.
• Forgetting. We can discard (purge) any soft clause.
• Hardening. We can reclassify any soft clause and call it hard.
• Softening. We can reclassify any hard clause $C$ and call it soft, provided that $\Phi$ is satisfiable whenever $\Phi \setminus C$ is satisfiable. In this case we also should output any necessary erp which which changes the settings of variables in such a way that any solution to $\Phi \setminus C$ becomes a solution to $\Phi$.

a) Prove that, throughout any such procedure, $F$ is satisfiable $\iff$ $\Phi$ is satisfiable $\iff$ $\Phi \cup \Psi$ is satisfiable.

b) Furthermore, given any solution to $\Phi$, we obtain a solution to $F$ by applying the erp rules in reverse order.

c) What is wrong with the following scenario? Start with one hard clause, $(x)$, and no soft clauses. Reclassify $(x)$ as soft, using the erp rule $x \leftarrow 1$. Then append a new soft clause $(\bar{x})$.

d) If $C$ is certifiable for $\Phi$ (see exercise 385), can we safely learn $C$?

e) If $C$ is certifiable for $\Phi \setminus C$, can we safely forget $C$?

f) In what cases is it legitimate to discard a clause, hard or soft, that is subsumed by another clause, hard or soft?

g) In what cases is self-subsumption permissible?

h) Explain how to eliminate all clauses that involve a particular variable $x$.

i) Show that, if $z$ is a new variable, we can safely learn the three new soft clauses $(x \vee z)$, $(y \vee z)$, $(\bar{x} \vee \bar{y} \vee \bar{z})$ in Tseytin's concept of extended resolution.

Verified: no
Solve time: 7m59s

---

Solution

Let the state of the inprocessing procedure be $(\Phi,\Psi)$. We prove that the invariant

$$ F\text{ is satisfiable}\iff \Phi\text{ is satisfiable}\iff \Phi\cup\Psi\text{ is satisfiable} $$

is preserved by every allowed operation.

For learning, suppose that $C$ is appended to $\Psi$. The hypothesis of learning says that

$$ \Phi\cup\Psi\cup{C} $$

is satisfiable whenever

$$ \Phi\cup\Psi $$

is satisfiable. Since adding a clause cannot create a satisfying assignment, the two formulas have the same satisfiability status. The hard part $\Phi$ is unchanged, so the invariant remains valid.

For forgetting, suppose that $C\in\Psi$ is removed, and write

$$ \Psi'=\Psi\setminus{C}. $$

The new hard set is still $\Phi$. Since $\Phi\cup\Psi$ was satisfiable exactly when $\Phi$ was satisfiable, there is a satisfying assignment of $\Phi\cup\Psi$ whenever $\Phi$ is satisfiable. That assignment satisfies every clause of $\Psi'$, because $\Psi'$ is a subset of $\Psi$. Hence

$$ \Phi\text{ satisfiable}\implies \Phi\cup\Psi'\text{ satisfiable}. $$

The converse implication holds because every satisfying assignment of $\Phi\cup\Psi'$ also satisfies all clauses of $\Phi$. Therefore

$$ \Phi\text{ satisfiable}\iff\Phi\cup\Psi'\text{ satisfiable}. $$

The equivalence with $F$ is unchanged because $\Phi$ is unchanged.

For hardening, a clause $C\in\Psi$ is moved into $\Phi$. The union of the two parts remains identical:

$$ \Phi'\cup\Psi'=\Phi\cup\Psi. $$

Therefore the satisfiability status of the total database is unchanged, and the hard set remains equivalent in satisfiability because every clause of the old soft set is now included among the hard clauses.

For softening, suppose that $C\in\Phi$ is moved into $\Psi$. The new sets are

$$ \Phi'=\Phi\setminus{C},\qquad \Psi'=\Psi\cup{C}. $$

The hypothesis for softening gives

$$ \Phi'\text{ satisfiable}\implies\Phi\text{ satisfiable}. $$

The reverse implication is immediate because every satisfying assignment of $\Phi$ satisfies all clauses of $\Phi'$. Hence

$$ \Phi'\text{ satisfiable}\iff\Phi\text{ satisfiable}. $$

Also,

$$ \Phi'\cup\Psi'

(\Phi\setminus{C})\cup(\Psi\cup{C})

\Phi\cup\Psi . $$

Thus the total formula is unchanged, while the satisfiability status of the hard part is unchanged. The erp rule associated with the softening step supplies a transformation from solutions of $\Phi'$ to solutions of $\Phi$, so the reconstruction of assignments is also preserved.

Therefore all four operations preserve

$$ F\text{ satisfiable}\iff\Phi\text{ satisfiable}\iff\Phi\cup\Psi\text{ satisfiable}. $$

For part (b), consider a sequence of operations that ends with a satisfying assignment of the final hard set $\Phi$. Clauses that were hardened are already included in this final hard set, so they are satisfied. The only clauses of $F$ that may fail to be present in $\Phi$ are clauses that were softened.

Each softening operation removed a clause $C$ from the hard set and recorded an erp rule that transforms every satisfying assignment of the reduced hard set into one satisfying $C$. Apply these erp rules in the reverse order of the original softening operations. At the moment a reversed rule is applied, all clauses that were restored later in the original computation are already present, so the assignment remains a solution of the current hard set. After all reverse transformations have been applied, every clause that was originally in $F$ is satisfied.

Thus every solution of the final $\Phi$ can be converted into a solution of $F$ by applying the erp rules in reverse order.

For part (c), the initial state is

$$ \Phi={x},\qquad \Psi=\varnothing . $$

After softening $(x)$, the state becomes

$$ \Phi=\varnothing,\qquad \Psi={x}. $$

The erp rule

$$ x\leftarrow1 $$

is valid because the empty hard formula has satisfying assignments, and setting $x=1$ produces a solution satisfying the removed clause.

The learning step for $(\bar{x})$ is not permitted. Before this step,

$$ \Phi\cup\Psi={x} $$

is satisfiable. After appending $(\bar{x})$,

$$ \Phi\cup\Psi={x,\bar{x}}, $$

which is unsatisfiable. The required implication for learning fails.

For part (d), suppose that $C$ is certifiable for $\Phi$. By the definition used in exercise 385, certification gives a derivation showing that

$$ \Phi\models C. $$

Every satisfying assignment of $\Phi$ therefore satisfies $C$. Consequently,

$$ \Phi\text{ satisfiable}\iff\Phi\cup{C}\text{ satisfiable}. $$

Since $C$ may be added as a soft clause without changing the satisfiability of the current database, $C$ can be safely learned.

For part (e), suppose that $C$ is certifiable for $\Phi\setminus C$. Then

$$ \Phi\setminus C\models C . $$

Hence every satisfying assignment of $\Phi\setminus C$ also satisfies $C$, and therefore

$$ \Phi\setminus C\text{ satisfiable}\iff\Phi\text{ satisfiable}. $$

If $C$ is a soft clause, forgetting it replaces $\Psi$ by $\Psi\setminus{C}$. Since every satisfying assignment of the remaining hard clauses already satisfies $C$, removing $C$ does not change satisfiability. Therefore such a clause can be safely forgotten.

For part (f), let $C$ be subsumed by $D$, so that

$$ D\subseteq C. $$

Every assignment satisfying $D$ also satisfies $C$. Therefore $C$ is redundant if $D$ remains in the formula that is required to preserve satisfiability.

If $C$ is soft, it may be forgotten when the subsuming clause $D$ remains in $\Phi\cup\Psi$, because every satisfying assignment of the new database satisfies $C$ as well.

If $C$ is hard, discarding it changes the hard set. This is legitimate only when the remaining hard clauses still imply $C$, which occurs in particular when a hard clause $D$ subsumes it. A subsuming soft clause is insufficient for removing a hard clause, because the hard satisfiability condition concerns $\Phi$ itself.

For part (g), a self-subsumption step replaces a clause by another clause obtained through resolution with a second clause. Such a replacement is valid only when the new partition of hard and soft clauses continues to satisfy the invariant.

For example, if a hard clause is replaced by a logically equivalent hard representation, the operation is safe. If a shorter clause is derived from the current database, it may be learned as a soft clause provided that the learning condition is satisfied. The original soft clause may then be forgotten only if the remaining database continues to satisfy the invariant. The transformations of exercises 379 and 380 are valid because their individual replacements preserve satisfiability, not merely because the shortened clauses are consequences.

For part (h), to eliminate a variable $x$, divide the clauses containing $x$ or $\bar{x}$ into three groups. Let

$$ C_1,\ldots,C_r $$

be the clauses containing $x$, and let

$$ D_1,\ldots,D_s $$

be the clauses containing $\bar{x}$.

For every pair $(C_i,D_j)$, form the resolvent

$$ (C_i\setminus{x})\cup(D_j\setminus{\bar{x}}). $$

Add all such resolvents to the database. Then remove every clause containing $x$ or $\bar{x}$. Clauses containing only positive occurrences of $x$ or only negative occurrences of $x$ cause no difficulty, because they disappear after the variable is removed.

The resolution construction preserves satisfiability: any assignment satisfying the original clauses satisfies all resolvents, and any assignment satisfying all resolvents can be extended to a value of $x$ that satisfies the removed clauses. The resulting database is therefore equisatisfiable with the original one. In an inprocessing solver, the new clauses must be classified as hard or soft in a way that preserves the invariant.

For part (i), let $z$ be a new variable. The three clauses

$$ (x\vee z),\qquad(y\vee z),\qquad(\bar{x}\vee\bar{y}\vee\bar{z}) $$

are the Tseytin encoding of

$$ z=x\land y . $$

If $x=y=1$, the first two clauses reduce to $z$, so they force

$$ z=1. $$

If $x=0$ or $y=0$, at least one of the first two clauses is automatically satisfied. The third clause forbids the case

$$ x=y=z=1, $$

so when $x=y=1$ it agrees with the forced value $z=1$.

More directly, the clauses imply $z\Rightarrow x$ and $z\Rightarrow y$ because if $z=1$, the first two clauses force $x=1$ and $y=1$. They also imply $x\land y\Rightarrow z$, because $x=y=1$ forces $z=1$. Hence the three clauses are satisfiable exactly for extensions satisfying

$$ z=x\land y . $$

Because $z$ is a new variable, every assignment to the old variables has a suitable extension with a value of $z$ precisely when the original formula has a satisfying assignment. Adding these three clauses therefore preserves satisfiability, so they may be learned as soft clauses.

This completes the proof.

$$ \boxed{\phantom{\text{answer}}} $$

∎