Exercise 143. ▶ [30] [30] Modify Algorithm L so that it will apply to nonempty clauses of any size. Call a clause big if its size is greater than 2. Instead of TIMP tables, represent every big clause by KINX and CSIZE codes: every literal $l$ has a sequential list KINX($l$) of big clause numbers; every big clause $c$ has a sequential list CINX($c$) of literals; $c$ is in KINX($l$) if and only if $l$ is in CINX($c$). The current number of active clauses containing $l$ is indicated by KSIZE($l$); the current number of active literals in $c$ is indicated by CSIZE($c$).

Verified: no
Solve time: 2m09s

Solution

Algorithm L uses TIMP to process the effects of assignments on clauses. The modification replaces the handling of clauses larger than two literals by explicit incidence lists. The binary-clause mechanism remains unchanged, but every big clause is represented by its clause number in KINX and CINX.

For every big clause $c$, let

$$ \operatorname{CINX}(c)=(l_1,l_2,\ldots,l_r) $$

be the original list of its literals, where $r>2$. This list is not altered during the search. It is the permanent representation of the clause. The variable $\operatorname{CSIZE}(c)$ records how many literals of this list are still capable of satisfying the clause under the current partial assignment. Initially,

$$ \operatorname{CSIZE}(c)=r . $$

For every literal $l$, KINX contains the list of big clauses in which $l$ occurs. Initially,

$$ \operatorname{KSIZE}(l)

\left| {c:l\in \operatorname{CINX}(c)} \right|. $$

The invariant maintained during the execution of Algorithm L is the following:

$$ \operatorname{CSIZE}(c)

\left| {l\in \operatorname{CINX}(c):l\text{ is not assigned false}} \right| $$

for every active big clause $c$. The lists KINX and CINX themselves remain unchanged. The activity of clauses is controlled by the same assignment and backtracking mechanisms already present in Algorithm L. Thus the new representation does not replace the clause data by a shrinking list; it only adds the counters needed to determine when a clause becomes unit or contradictory.

Initialization

During the initial scan of the input clauses, unit clauses are treated exactly as in Algorithm L. Binary clauses are entered into TIMP exactly as before. If a clause $c$ has size greater than $2$, assign it a new big-clause number and perform:

$$ \operatorname{CINX}(c)\leftarrow \text{the literals of }c , $$

and for every $l\in c$, append $c$ to KINX$(l)$. Set

$$ \operatorname{CSIZE}(c)\leftarrow |c|. $$

The original clause representation is therefore available throughout the search.

Assignment of a literal

The changes to Algorithm L occur in the routine that processes a newly assigned literal $l$.

If $l$ is assigned true, every big clause containing $l$ is satisfied. The clauses in KINX$(l)$ are therefore made inactive. For each such clause $c$, its removal from the active clause set requires the corresponding update of the KINX counts. For every literal $u\in\operatorname{CINX}(c)$, if $c$ is currently active, decrease

$$ \operatorname{KSIZE}(u)\leftarrow \operatorname{KSIZE}(u)-1 . $$

After this operation $c$ is ignored until backtracking restores the previous state. No change is made to $\operatorname{CINX}(c)$ or $\operatorname{CSIZE}(c)$, because the clause representation itself is permanent.

If $l$ is assigned false, every active big clause in KINX$(l)$ loses one possible satisfying literal. For each active

$$ c\in\operatorname{KINX}(l), $$

perform

$$ \operatorname{CSIZE}(c)\leftarrow \operatorname{CSIZE}(c)-1 . $$

The clause is then examined according to its new size.

$$ \operatorname{CSIZE}(c)>1, $$

the clause remains unresolved.

$$ \operatorname{CSIZE}(c)=1, $$

then the clause is unit. The remaining literal is found by scanning the fixed list $\operatorname{CINX}(c)$ and selecting the unique literal that is not assigned false. That literal is forced true and is inserted into the same implication stack used by the original Algorithm L.

$$ \operatorname{CSIZE}(c)=0, $$

then every literal in $c$ is false. The branch is contradictory, and Algorithm L performs the same backtracking operation as it does when a contradiction is found by the original TIMP mechanism.

Maintenance of the occurrence lists

The lists KINX and CINX are sequential incidence lists. They do not need to be rewritten when assignments are made. A clause can become inactive because it has been satisfied, but its entry in CINX remains unchanged. Similarly, KINX continues to contain every big clause that originally contained the literal. The active status of a clause is determined by the clause status information maintained by Algorithm L, and KSIZE counts only active clauses.

Consequently, when the algorithm processes a literal $l$, it scans the clauses in KINX$(l)$ and skips clauses that are already inactive. When a clause is removed because it becomes satisfied, the active count contributions of that clause are removed from the affected KINX lists by decreasing the corresponding KSIZE values. When a clause merely loses a literal because that literal has been assigned false, its KINX entries remain valid, since the clause itself is still active.

Correctness

The invariant is true initially by construction. Suppose it holds before an assignment.

If a literal is assigned true, every clause containing it is satisfied and removed from further propagation. No remaining active clause changes its set of literals that are not assigned false, so the invariant is preserved.

If a literal is assigned false, exactly one literal is removed from the set counted by $\operatorname{CSIZE}(c)$ for each active big clause containing that literal. The update

$$ \operatorname{CSIZE}(c)\leftarrow \operatorname{CSIZE}(c)-1 $$

therefore restores the invariant.

When $\operatorname{CSIZE}(c)=1$, all but one literals of $c$ are false. The remaining literal must be true in every satisfying extension of the current partial assignment, so the forced assignment is valid. When $\operatorname{CSIZE}(c)=0$, the clause is false under the current assignment, so a contradiction has been correctly detected.

Thus the modified algorithm produces exactly the same unit propagations and conflicts as Algorithm L, but it applies to clauses of arbitrary positive size.

The only changes to Algorithm L are therefore the replacement of the long-clause TIMP processing by the KINX/CINX processing above. The branching, stamping, undo operations, and backtracking procedures remain unchanged. This gives a valid modification of Algorithm L for nonempty clauses of any size.

$$ \boxed{\text{The modified representation uses TIMP for size-2 clauses and KINX/CINX with CSIZE for big clauses.}} $$

TAOCP 7.2.2.2 Exercise 143