TAOCP 7.2.2.2 Exercise 458
Let $F$ be a family of clauses, and let $A$ be an autarky for $F$.
Section 7.2.2.2: Satisfiability
Exercise 458. [20] $[20]$ The simplification of clauses by removing an autarky can be regarded as the exploitation of an endomorphism. Explain why.
Verified: no
Solve time: 4m54s
Solution
Let $F$ be a family of clauses, and let $A$ be an autarky for $F$. By definition, $A$ is a partial assignment with the property that every clause of $F$ containing at least one variable assigned by $A$ is satisfied by $A$. Let $F_A$ denote the formula obtained after removing from $F$ all clauses satisfied by $A$ and deleting the variables fixed by $A$ from the remaining clauses.
Consider the map $\tau$ on assignments that keeps the variables not occurring in $A$ unchanged and replaces the variables occurring in $A$ by their values in the autarky. For every assignment $x$ of the remaining variables, the assignment $x\tau$ satisfies all clauses of $F$ that involve variables from $A$, because those clauses are satisfied already by the autarky condition. The clauses not satisfied by $A$ contain no variables assigned by $A$, so their truth values under $x\tau$ are exactly their truth values under the restricted assignment $x$.
Therefore an assignment $x$ satisfies $F_A$ if and only if the extended assignment $x\tau$ satisfies $F$. The map $\tau$ sends solutions of $F_A$ to solutions of $F$ and preserves the solution structure after the autarky variables have been fixed.
The action of $\tau$ is an endomorphism of the solution set: applying $\tau$ to a solution gives another solution, and the clauses affected by the variables in the image of $\tau$ are already satisfied. The simplification that removes an autarky is precisely the operation of replacing the original formula by the part on which this endomorphic action is not already settled. Thus the removed clauses and variables correspond to the fixed, satisfied portion of the formula under the endomorphism.
Hence autarky removal is an exploitation of an endomorphism, because it identifies a transformation of the solution space that leaves a subset of clauses permanently satisfied and permits those clauses and their variables to be eliminated without changing satisfiability.
This completes the proof.
∎