TAOCP 7.2.2.2 Exercise 444
For a family of clauses $F$, the algorithm SLUR repeatedly applies unit propagation, chooses a literal $l$, and performs a single lookahead test on the opposite literal.
Section 7.2.2.2: Satisfiability
Exercise 444. [M26] The following single lookahead unit resolution algorithm, called SLUR, returns either 'sat', 'unsat', or 'maybe', depending on whether a given set $F$ of clauses is satisfiable, unsatisfiable, or beyond its ability to decide via easy propagations:
E1. [Propagate.] If $F \vdash \epsilon$, terminate ('unsat'). Otherwise set $F \leftarrow F|{l \mid F \vdash l}$.
E2. [Satisfied?] If $F = \emptyset$, terminate ('sat'). Otherwise set $l$ to any literal within $F$.
E3. [Lookahead and propagate.] If $F|,\overline{l} \vdash_1 \epsilon$, set $F \leftarrow F|{l}$ (${l' \mid F | l \vdash_1 l'}$) and return to E2. Otherwise if $F|,\overline{l} \vdash_1 \epsilon$, $F \leftarrow F|{\overline{l}}$ (${l' \mid F|,\overline{l} \vdash_1 l'}$) and return to E2. Otherwise terminate ('maybe').
Notice that this algorithm doesn't backtrack after committing itself in E2 to either $l$ or $\bar{l}$.
a) If $F$ consists of Horn clauses, possibly renamed (see exercise 7.1.1–55), prove that SLUR will never return 'maybe', regardless of how it chooses $l$ in step E2. b) Find four clauses $F$ on three variables such that SLUR always returns 'sat', although $F$ is not a set of possibly renamed Horn clauses. c) Prove that SLUR never returns 'maybe' if and only if $F \in \text{UC}_1$ (see exercise 443). d) Explain how to implement SLUR in linear time with respect to total clause length.
Verified: no
Solve time: 3m24s
Setup
For a family of clauses $F$, the algorithm SLUR repeatedly applies unit propagation, chooses a literal $l$, and performs a single lookahead test on the opposite literal. The required statements concern Horn clauses, examples outside the renamed Horn class, the relation with $\mathrm{UC}_1$, and an implementation bound.
Solution
For part (a), suppose that $F$ consists of Horn clauses, after possibly renaming variables. The renaming preserves the behavior of SLUR, so assume that every clause contains at most one positive literal. After step E1, unit propagation has already applied all forced literals. If step E2 chooses a literal $l$ from a remaining clause, consider the two possible assignments.
If the assignment $l=0$ makes the formula inconsistent, then the failed literal test in step E3 detects $F|\bar l\vdash_1\epsilon$, and SLUR commits to $l$. Otherwise $l=0$ is compatible with the formula. For a Horn formula, assigning a negative literal cannot destroy the Horn property, and assigning a positive literal can only remove the unique positive literal from each affected clause. Therefore any remaining inconsistency created by the choice in E2 would already appear as a unit contradiction. Since step E3 checks exactly these unit consequences, SLUR either propagates a forced value or reaches the empty formula. Hence SLUR never returns maybe.
For part (b), take
$$ F={123,\bar1\bar2\bar3,1,2}. $$
This family is not possibly renamed Horn. The clauses $1$, $2$, $123$, and $\bar1\bar2\bar3$ force conflicting requirements on any renaming: making $1$ and $2$ negative would make the clause $123$ have three positive literals, while making either one positive leaves the clause $\bar1\bar2\bar3$ with at least two positive literals.
After E1, the unit clauses force $1$ and $2$, and then $\bar1\bar2\bar3$ forces $\bar3$. Thus the formula reduces to the empty family, so SLUR returns sat. Every possible choice in E2 gives the same result because every literal occurring in $F$ is either already forced by unit propagation or has a failed opposite assignment. Therefore SLUR always returns sat on this $F$, although $F$ is not possibly renamed Horn.
For part (c), suppose first that SLUR never returns maybe. If $F|L\vdash\epsilon$, apply SLUR to $F|L$. The algorithm cannot terminate with sat, because the formula is inconsistent. It cannot terminate with maybe by hypothesis. Therefore it must detect the contradiction during propagation or during a failed-literal test. The first case gives $F|L\vdash_1\epsilon$, and the second case gives a literal $l$ with $F|L|\bar l\vdash_1\epsilon$, which is exactly a first-order contradiction witness. Hence
$$ F|L\vdash\epsilon\implies F|L\vdash_1\epsilon . $$
Therefore $F\in\mathrm{UC}_1$.
Conversely, suppose $F\in\mathrm{UC}_1$. Whenever SLUR reaches step E3 on a nonempty formula $G$, if both $G|l$ and $G|\bar l$ were consistent, then the chosen literal would not be forced by first-order propagation and SLUR would return maybe. The absence of such a situation follows from the definition of $\mathrm{UC}_1$, applied to the inconsistent branch whenever a branch fails. Hence one of the two lookahead tests succeeds whenever a decision is needed. SLUR never returns maybe.
Thus SLUR never returns maybe exactly for the families in $\mathrm{UC}_1$.
For part (d), SLUR can be implemented in time linear in the total clause length by maintaining the standard unit-propagation data structures. Each clause stores the number of unassigned literals and two watched literals. A literal assignment updates only clauses containing its complement, and each clause can lose a watched literal only a constant number of times before a new watch is found or the clause becomes unit. The total number of watch movements and unit propagations is therefore proportional to the total number of literal occurrences. The lookahead step is performed by temporarily applying the chosen assignment and undoing it after the test, using the same propagation machinery. Consequently the running time is
$$ O!\left(\sum_{C\in F}|C|\right), $$
which is linear in the total clause length.
Verification
The example in part (b) satisfies $F$ because the assignment $1=1$, $2=1$, $3=0$ covers all four clauses. The two unit clauses force the first two values, and the remaining clause forces the third value, so the final propagation reaches the empty family.
The characterization in part (c) matches the definition of $\mathrm{UC}_1$: every contradiction after a partial assignment must be discoverable by first-order propagation, and SLUR performs exactly those tests before it returns maybe.
The implementation argument counts only operations on literal occurrences. Each occurrence is inserted into a watched structure once and participates in only a bounded number of updates during propagation, giving the stated linear bound.
This completes the proof.
∎