Section 7.2.2.2: Satisfiability

Exercise 165. ▶ [26] [26] Design an algorithm to find the largest positive autarky $A$ for a given $F$, namely an autarky that contains only positive literals. Hint: Warm up by finding the largest positive autarky for the clauses ${123, 125, 134, 136, 145, 156, 235, 246, 345, 356}$.

Verified: yes
Solve time: 2m37s

---

The previous maximality argument fails because it tries to compare an arbitrary autarky $B$ with intermediate sets $A_t$ by reasoning about individual clause-triggered deletions. That step is invalid since a clause that is “bad” for $A_t$ may not be “bad” for $B$. The correct proof must instead use a monotone operator and a greatest fixed-point argument.

Reformulation

Let $F$ be a set of clauses over variables $x_1,\dots,x_n$. For a clause $C$, write $\mathrm{pos}(C)$ for the set of variables appearing positively in $C$.

A set $A \subseteq {x_1,\dots,x_n}$ is a positive autarky iff

$$ \forall C \in F:\quad C \cap A \neq \emptyset ;\Rightarrow; \mathrm{pos}(C)\cap A \neq \emptyset. $$

Equivalently, no clause intersects $A$ only in negatively occurring variables.

Step 1: Define the elimination operator

For $A \subseteq V$, define the set of bad variables

$$ \mathrm{Bad}(A)

\bigcup \left{ C \cap A ;:; C \cap A \neq \emptyset \ \wedge\ \mathrm{pos}(C)\cap A = \emptyset \right}. $$

Define the operator

$$ T(A) = A \setminus \mathrm{Bad}(A). $$

Thus $T(A)$ removes from $A$ exactly those variables that lie in a clause that currently has no supporting positive literal in $A$.

Step 2: Basic properties of $T$

(1) $T(A) \subseteq A$

Immediate from definition.

(2) Monotonicity

If $A \subseteq B$, then $T(A) \subseteq T(B)$.

Proof. Let $x \in T(A)$. Then $x \in A \subseteq B$. We show $x \notin \mathrm{Bad}(B)$.

Assume for contradiction that $x \in \mathrm{Bad}(B)$. Then there exists a clause $C$ such that

$$ x \in C,\quad C \cap B \neq \emptyset,\quad \mathrm{pos}(C)\cap B = \emptyset. $$

Since $A \subseteq B$,

$$ C \cap A \neq \emptyset,\quad \mathrm{pos}(C)\cap A = \emptyset, $$

so $x \in \mathrm{Bad}(A)$, contradicting $x \in T(A)$. Hence $x \in T(B)$. ∎

Thus $T$ is monotone.

Step 3: Iteration and existence of a fixed point

Start with

$$ A_0 = {x_1,\dots,x_n}, \qquad A_{t+1} = T(A_t). $$

Since $A_{t+1} \subseteq A_t$, the sequence stabilizes after at most $n$ steps. Let

$$ A^* = A_t \quad \text{for sufficiently large } t, $$

so $T(A^) = A^$. Hence $A^*$ is a fixed point.

By construction, $A^*$ satisfies the autarky condition, because no clause can witness a violation without triggering further removal.

Step 4: Key corrected maximality argument

We prove that every positive autarky is contained in $A^*$.

Lemma: every positive autarky is a post-fixed point

Let $B$ be a positive autarky. Then

$$ B \subseteq T(B). $$

Proof. Take $x \in B$. Suppose $x \notin T(B)$. Then $x \in \mathrm{Bad}(B)$, so there exists a clause $C$ such that

$$ x \in C,\quad C \cap B \neq \emptyset,\quad \mathrm{pos}(C)\cap B = \emptyset. $$

This contradicts that $B$ is a positive autarky, since $C\cap B \neq \emptyset$ would require $\mathrm{pos}(C)\cap B \neq \emptyset$. Hence $x \in T(B)$. ∎

Thus every positive autarky is a post-fixed point of $T$.

Lemma: iteration from the top yields the greatest fixed point

Since $T$ is monotone on the finite lattice $(2^V,\subseteq)$, the limit $A^*$ is the greatest fixed point of $T$ (Knaster–Tarski theorem for finite posets).

Therefore, for every $B \subseteq V$,

$$ B \subseteq T(B) ;\Rightarrow; B \subseteq A^*. $$

Conclusion (maximality)

Every positive autarky $B$ satisfies $B \subseteq A^$. Hence $A^$ contains all positive autarkies and is therefore the largest positive autarky.

Final algorithm

1. Initialize $A \leftarrow {x_1,\dots,x_n}$.
2. Repeat:

• Delete every $x \in A$ such that there exists a clause $C$ with

$$ x \in C,\quad C \cap A \neq \emptyset,\quad \mathrm{pos}(C)\cap A = \emptyset. $$ 3. Stop when no change occurs. 4. Output $A$.

This runs in polynomial time since each iteration removes at least one variable and checking clauses can be done in polynomial total work.

Key correction over the flawed proof

The incorrect step was attempting to show that deleted variables cannot belong to another autarky by analyzing a single deletion step. The correct argument avoids this entirely and instead shows:

• every autarky is a post-fixed point of a monotone operator,
• the algorithm computes the greatest fixed point of that operator,
• hence it contains every autarky.