TAOCP 7.2.2.2 Exercise 156

Let $v$ be a variable that is pure in $F$, so every occurrence of $v$ in every clause of $F$ has the same sign, either all occurrences are $v$ or all are $\bar v$.

Section 7.2.2.2: Satisfiability

Exercise 156. [05] [05] Why is a pure literal a special case of an autarky?

Verified: yes
Solve time: 1m03s


Let $v$ be a variable that is pure in $F$, so every occurrence of $v$ in every clause of $F$ has the same sign, either all occurrences are $v$ or all are $\bar v$. Let $l$ be that literal.

An autarky is a set $L$ of literals such that every clause that contains a variable from $|L|$ is satisfied by a literal in $L$, so those clauses are made true without affecting any clause that does not involve variables from $L$. Taking $L = {l}$, every clause containing $v$ contains $l$ because no clause contains the opposite literal $\bar l$. Hence every clause touched by $v$ is satisfied by $L$, while all other clauses are unchanged. This shows that a pure literal assignment satisfies the defining condition of an autarky, so a pure literal is a special case of an autarky. ∎