TAOCP 7.2.2.2 Exercise 165

Let $F$ be a $k$SAT formula with variables $x_1,\ldots,x_n$.

taocpmathematicsalgorithmsvolume-4hard

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: 1m46s

Setup

Let $F$ be a $k$SAT formula with variables $x_1,\ldots,x_n$. For a clause $C$, write $P(C)$ for the set of variables whose positive literals occur in $C$, and write $N(C)$ for the set of variables whose negative literals occur in $C$.

A positive autarky is a set $A$ of variables, interpreted as the partial assignment that sets every variable in $A$ to true and leaves every other variable unset. The condition for $A$ to be an autarky is that every clause containing a variable of $A$ contains at least one positive literal whose variable is in $A$.

The goal is to find a largest such set $A$.

Solution

Start with

$$ A\leftarrow {x_1,\ldots,x_n}. $$

Repeatedly perform the following operation. If there is a clause $C$ such that

$$ P(C)\cap A=\emptyset $$

and

$$ N(C)\cap A\ne\emptyset, $$

replace

$$ A\leftarrow A\setminus N(C). $$

Continue until no such clause exists. The remaining set $A$ is the required largest positive autarky.

The procedure terminates because every replacement removes at least one variable from $A$, and there are only $n$ variables.

It remains to prove that the final set is correct. First consider any set $A$ produced when the procedure stops. For every clause $C$ with

$$ N(C)\cap A\ne\emptyset, $$

the stopping condition implies

$$ P(C)\cap A\ne\emptyset. $$

Thus every clause touched by the partial assignment $A$ contains a positive literal set to true by that assignment. Hence every touched clause is satisfied, so $A$ is a positive autarky.

Now we prove maximality. During the algorithm, the current set $A$ only decreases. Suppose that at some stage a clause $C$ satisfies

$$ P(C)\cap A=\emptyset $$

and

$$ N(C)\cap A\ne\emptyset. $$

Let $B\subseteq A$ be any positive autarky contained in the current set. If $B$ contained some variable $x\in N(C)\cap A$, then $C$ would be touched by $B$, because $x$ occurs in $C$. However, since

$$ P(C)\cap A=\emptyset, $$

there is no variable of $B$ occurring positively in $C$. The clause $C$ would therefore not be satisfied by the partial assignment $B$, contradicting that $B$ is an autarky.

Therefore every positive autarky contained in the current set must avoid every variable in $N(C)$. Removing $N(C)$ cannot remove any variable that belongs to a possible positive autarky extending the current one.

Initially the current set is the set of all variables, so the preceding argument applies to every positive autarky. Every deletion made by the algorithm removes only variables that cannot occur in any positive autarky. When the algorithm terminates, the remaining set itself is a positive autarky, and every positive autarky is contained in it. Hence it is the largest positive autarky.

For the warm-up instance

$$ {123,125,134,136,145,156,235,246,345,356}, $$

every clause contains only positive literals. The set

$$ A={1,2,3,4,5,6} $$

satisfies the stopping condition immediately, because every clause contains a positive literal from $A$. Since no positive autarky can contain more than all variables, this is the largest positive autarky for the example.

This completes the proof.

∎

Verification

The algorithm has two possible outcomes for each clause. If a clause contains a selected variable negatively, then either it also contains a selected variable positively, in which case it is satisfied, or the algorithm deletes all selected variables that occur negatively in that clause. The second case is precisely the only situation in which those variables cannot belong to any positive autarky that remains possible.

The final set is therefore characterized by the condition

$$ N(C)\cap A\ne\emptyset\implies P(C)\cap A\ne\emptyset $$

for every clause $C$, which is exactly the autarky condition for a positive partial assignment. The construction and maximality argument establish that the returned set is the unique largest positive autarky.