TAOCP 7.2.2.2 Exercise 162

Section 7.2.2.2: Satisfiability

Exercise 162. [21] [21] Devise an efficient way to discover all of the (a) blocked binary clauses ($\bar{l} \vee a$) and (b) size-two autarkies $A = {a, a'}$ of a given kSAT problem $F$.

Verified: yes
Solve time: 2m42s

---

Corrected Solution

(a) Blocked binary clauses $(\bar l \vee a)$

Definition

A clause $C$ is blocked by a literal $u \in C$ if for every clause $D \in F$ containing $\bar u$, the resolvent

$$ (C \setminus {u}) \cup (D \setminus {\bar u}) $$

is a tautology, meaning it contains some literal $x$ together with its complement $\bar x$.

We apply this to the binary clause

$$ C = (\bar l \vee a). $$

There are two possible blocking literals: $u = \bar l$ or $u = a$.

We assume standard CNF input where clauses are non-tautological (no clause contains both $x$ and $\bar x$). This is without loss of generality since tautological clauses can be discarded.

Case 1: $u = \bar l$

We resolve $C$ with any clause $D$ containing $l$. The resolvent is

$$ R = {a} \cup (D \setminus {l}). $$

Since $D$ is not tautological, the only way for $R$ to be a tautology is that it contains both $x$ and $\bar x$. The only way the singleton literal $a$ participates in such a pair is if $\bar a \in D$.

Thus, for every clause $D$ containing $l$, we must have $\bar a \in D$. Hence:

$$ \operatorname{Occ}(l) \subseteq \operatorname{Occ}(\bar a). $$

Case 2: $u = a$

We resolve $C$ with any clause $D$ containing $\bar a$. The resolvent is

$$ R = {\bar l} \cup (D \setminus {\bar a}). $$

Again, since $D$ is non-tautological, $R$ is a tautology only if it contains both $x$ and $\bar x$. This forces $l \in D$.

Thus:

$$ \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(l). $$

Characterization

The clause $(\bar l \vee a)$ is blocked if and only if at least one of its literals blocks it, hence:

$$ \operatorname{Occ}(l) \subseteq \operatorname{Occ}(\bar a) \quad \text{or} \quad \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(l). $$

Efficient discovery

1. Build occurrence lists $\operatorname{Occ}(l)$ for all literals in one scan of $F$.
2. For each clause $(\bar l \vee a)$, test:

• whether every clause in $\operatorname{Occ}(l)$ contains $\bar a$, or
• whether every clause in $\operatorname{Occ}(\bar a)$ contains $l$.

Each test is performed by scanning the relevant occurrence list with constant-time membership checks per clause. This yields all blocked binary clauses.

(b) Size-two autarkies $A = {a, a'}$

Definition

A set of literals $A$ is an autarky if every clause containing any literal whose variable appears in $A$ is already satisfied by $A$, i.e., the clause contains at least one literal from $A$.

Thus $A = {a, a'}$ is an autarky if and only if every clause satisfies:

$$ (C \cap {\pm \mathrm{var}(a), \pm \mathrm{var}(a')} \neq \emptyset) ;\Rightarrow; (C \cap {a, a'} \neq \emptyset). $$

Equivalently:

• Any clause containing $a$ or $a'$ is satisfied immediately.
• Any clause containing $\bar a$ or $\bar a'$ must also contain $a$ or $a'$.

Explicit condition

We split by literals.

Clauses containing $\bar a$

Every clause $C$ with $\bar a \in C$ must satisfy:

$$ C \cap {a, a'} \neq \emptyset. $$

Since $a \notin C$, this reduces to:

$$ a' \in C. $$

So:

$$ \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(a'). $$

Clauses containing $\bar a'$

Similarly:

$$ \operatorname{Occ}(\bar a') \subseteq \operatorname{Occ}(a). $$

Characterization

A pair $A = {a, a'}$ is an autarky if and only if:

$$ \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(a') \quad \text{and} \quad \operatorname{Occ}(\bar a') \subseteq \operatorname{Occ}(a). $$

Efficient enumeration

1. Build all occurrence lists for literals in one scan of $F$.
2. For each pair of literals $a, a'$ that appear in $F$:

• Test whether every clause in $\operatorname{Occ}(\bar a)$ contains $a'$.
• Test whether every clause in $\operatorname{Occ}(\bar a')$ contains $a$.

Each test uses only scans of occurrence lists with constant-time clause membership checks.

All valid size-two autarkies are exactly those pairs passing both tests.

Summary

• A binary clause $(\bar l \vee a)$ is blocked iff one literal’s occurrence set is contained in the occurrence set of the other’s complement:

$$ \operatorname{Occ}(l) \subseteq \operatorname{Occ}(\bar a) ;;\text{or};; \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(l). $$

• A pair ${a,a'}$ is an autarky iff:

$$ \operatorname{Occ}(\bar a) \subseteq \operatorname{Occ}(a') ;;\text{and};; \operatorname{Occ}(\bar a') \subseteq \operatorname{Occ}(a). $$

These conditions yield direct and efficient enumeration algorithms.