TAOCP 7.2.2.2 Exercise 159
A set $A$ of literals is an autarky for a family $F$ of clauses if every clause that contains a literal $l$ with $l \in A$ is satisfied by $A$.
Section 7.2.2.2: Satisfiability
Exercise 159. [M17] [M17] True or false: (a) $A$ is an autarky for $F$ if and only if $F \mid A \subseteq F$. (b) If $A$ is an autarky for $F$ and $A' \subseteq A$, then $A \setminus A'$ is an autarky for $F|A'$.
Verified: yes
Solve time: 1m18s
Solution
A set $A$ of literals is an autarky for a family $F$ of clauses if every clause that contains a literal $l$ with $l \in A$ is satisfied by $A$. Equivalently, whenever a clause contains some literal from $A$, that clause contains no literal from ${\bar{l} : l \in A}$ and hence is removed or satisfied when the partial assignment induced by $A$ is applied. The reduced formula $F \mid A$ is obtained from $F$ by deleting every clause satisfied by $A$ and deleting from the remaining clauses every literal whose complement lies in $A$.
(a)
The statement claims that $A$ is an autarky for $F$ if and only if $F \mid A \subseteq F$.
Take $F = \bigl{{1,2}\bigr}$ and $A = {\bar{1}}$. The set $A$ is an autarky for $F$ because the only clause ${1,2}$ contains no literal from $A$, so the defining condition is satisfied vacuously.
Applying $A$ to $F$ does not satisfy the clause ${1,2}$, and since the literal $1$ is not removed by $A$, no deletion occurs inside the clause. Hence $F \mid A = \bigl{{1,2}\bigr}$ after reduction rules that only remove literals whose complements lie in $A$, and since $\bar{1} \in A$, the literal $1$ is removed, giving $F \mid A = \bigl{{2}\bigr}$.
The clause ${2}$ is not an element of $F$, so $F \mid A \nsubseteq F$. This shows that the stated equivalence fails.
Thus (a) is false.
(b)
Assume $A$ is an autarky for $F$ and $A' \subseteq A$. Let $F' = F \mid A'$. The reduced formula $F'$ is obtained from $F$ by deleting all clauses satisfied by $A'$ and removing from remaining clauses all literals whose complements lie in $A'$.
Consider the set $A \setminus A'$. Take any clause $C$ of $F'$. By construction, $C$ is a clause of $F$ with all literals whose complements lie in $A'$ removed, and $C$ is not satisfied by $A'$.
If $C$ contains a literal from $A \setminus A'$, then it also contains a literal from $A$, since $A \setminus A' \subseteq A$. Since $A$ is an autarky for $F$, every clause of $F$ that contains a literal from $A$ is satisfied by $A$. Removing literals corresponding to $A'$ does not introduce falsification of any remaining literal from $A \setminus A'$, because satisfaction depends only on presence of a literal from $A$, not on other literals in the clause.
Therefore every clause of $F'$ that contains a literal from $A \setminus A'$ is satisfied by $A \setminus A'$. This matches the definition of autarky applied to $F'$.
Thus $A \setminus A'$ is an autarky for $F \mid A'$.
This completes the proof. ∎