TAOCP 7.2.2.2 Exercise 270

Section 7.2.2.2: Satisfiability

Exercise 270. [25] [25] (On-the-fly subsumption.) The intermediate clauses that arise in step C7, immediately before resolving with a reason $R_l$, occasionally turn out to be equal to the shorter clause $R_l \setminus l$. In such cases we have an opportunity to strengthen that clause by deleting $l$ from it, thus making it potentially more useful in the future.

a) Construct an example where two clauses can each be subsumed in this way while resolving a single conflict. The subsumed clauses should both contain two literals assigned at the current level of the trail, as well as one literal from a lower level.

b) Show that it's easy to recognize such opportunities, and to strengthen such clauses efficiently, by modifying the steps of answer 263.

Verified: no
Solve time: 10m53s

Correctness

The proposed solution addresses both parts of the exercise, but part (a) does not construct a valid example satisfying all of the stated conditions.

For part (a), the intended situation is that two different intermediate clauses arising during a single conflict analysis are each equal to $R_l\setminus l$ for their respective reason clauses. The proposed construction attempts this by using several propagated literals with similar reason clauses. The first subsumption opportunity is valid in isolation:

$$ C_1=(\bar m\vee\bar u\vee\bar v\vee\bar w) $$

is indeed equal to

$$ R_m\setminus m $$

for

$$ R_m=(m\vee\bar u\vee\bar v\vee\bar w). $$

However, the construction is then modified by introducing $n$ and changing the conflict clause. The first strengthened clause is no longer preserved in the same conflict analysis. The second construction does not actually demonstrate two clauses being subsumed in the required way, because after the first resolution sequence the clause

$$ C_1=(\bar m\vee\bar n\vee\bar u\vee\bar v\vee\bar w\vee\bar z) $$

is not equal to the original $R_m\setminus m$, since it contains the additional literal $\bar n$. The solution then asserts that the first two resolutions are unchanged except for extra literals remaining, but this destroys the equality needed for the first on-the-fly subsumption event.

For part (b), the general idea is correct. During step C7, the solver has the current intermediate clause and the reason clause $R_l$. Testing whether the intermediate clause equals $R_l\setminus l$ is the correct recognition criterion. If equality holds, replacing $R_l$ by $R_l\setminus l$ is valid because the shorter clause is a logical consequence of the old clause together with the current conflict-resolution context. The proposed solution correctly identifies that the necessary information is already present during conflict analysis.

The efficiency discussion is mostly correct, although it omits the concrete modifications to the steps of answer 263 requested by the exercise. The exercise asks for a modification of those steps, not only a conceptual description. A complete answer should specify where the equality test is inserted and how the clause data structures are updated.

Gaps and Errors

Invalid construction in part (a), Critical error.

The proposed solution claims that the second construction gives two strengthening opportunities in one conflict. It does not. After adding $n$, the clause obtained after resolving with $R_l$ is

$$ (\bar m\vee\bar n\vee\bar u\vee\bar v\vee\bar w\vee\bar z), $$

which is not equal to

$$ R_m\setminus m=(\bar u\vee\bar v\vee\bar w) $$

or even to the later modified version of $R_m\setminus m$, because of the extra literals $\bar n$ and $\bar z$. Thus the first strengthening opportunity disappears in the actual example being presented.

Failure to construct two simultaneous subsumptions, Critical error.

The exercise requires two clauses to each be subsumed while resolving a single conflict. The proposed solution first constructs one valid opportunity and then constructs a different conflict intended to create a second opportunity. It never gives a single conflict analysis containing two valid opportunities.

Missing justification of the propagation scenario, Justification gap.

The solution states that the clauses are "valid forcing clauses because the literals preceding $l$ and $m$ in the trail falsify all the other literals," but it does not specify a consistent trail order showing that both propagations can occur. In Algorithm C, the order of assignments matters, because a reason clause can only propagate a literal when all its other literals are already false. A complete construction must give a trail and levels compatible with both reasons.

Part (b) lacks the requested algorithm modification, Justification gap.

The recognition condition is correctly described, but the answer does not actually modify the steps of answer 263. A complete solution should state the additional operation in the conflict-analysis loop, such as checking before each resolution whether the current clause equals $R_l\setminus l$ and, if so, deleting $l$ from the stored clause and updating the watched-literal or occurrence data structures.

Claim that deleting $l$ preserves satisfiability is insufficiently justified, Justification gap.

The statement that $R_l$ can be replaced by $R_l\setminus l$ is not true for an arbitrary reason clause. The validity comes specifically from the fact that the current intermediate clause already implies $R_l\setminus l$ during the conflict derivation. The proposed solution gestures toward this but does not explain the logical implication carefully.

Summary

The solution has the right intuition for part (b) and correctly identifies the equality test that detects on-the-fly subsumption. However, the central construction required in part (a) is invalid: it does not exhibit two clauses that are both strengthened during the same conflict. The missing explicit modification of Algorithm C's conflict-analysis steps is an additional incompleteness.

VERDICT: FAIL, the proposed construction for part (a) does not actually produce two on-the-fly subsumption opportunities in a single conflict.