Conflict learning and backjumping (why you must record collapses)
Parent: recursive-harness
When the agent works down a sub-tree, hits a dead end, and traces back — two mechanisms are needed, and they are exactly the two pillars of CDCL (Conflict-Driven Clause Learning), the engine of modern SAT/CSP solvers.
① Non-chronological backjumping (the backtrack can land in another sub-tree)
On a conflict (a domain emptied), don't undo the most recent step. Instead:
- analyze the implication graph (which decisions + propagations produced the conflict) → compute the conflict set (the decision variables actually responsible);
- backjump to the most recent decision in the conflict set — which may live in a different sub-tree.
- Why cross-sub-tree: constraints cross sub-trees (mutual influence), so the conflict set can include other sub-trees' decisions. The backjump target is computed from the conflict, not from the tree structure.
② No-good / conflict-clause learning (the "collapse information")
From the conflict, derive a no-good — ¬(x₁=a ∧ x₅=b ∧ x₉=c) — and add it to C permanently. Propagation can never re-enter that combination: you've recorded which worlds collapsed.
Why "otherwise it can't converge" is exactly right:
Without learning, the search re-derives the same conflicts (thrashing), looping through equivalent dead branches → no monotone progress → blowup / non-convergence on hard instances. With learning, the no-good store grows monotonically: every conflict teaches something permanent, never repeated.
Key resolution (of the earlier monotone-vs-revision tension):
The assignment backtracks (non-monotone), but knowledge (the learned collapse-info) is monotone. Convergence comes from the monotonicity of knowledge, not of the assignment. Finite domains → the no-good space is finite → learning terminates → CDCL converges; infinite domains →
P×Cbounds it.
It operationalizes deducible ≠ known
deducible-not-known: constraints entail the answer, but deriving entailments is NP-hard — you can't compute the full closure. CDCL is the operational answer:
Clause learning = lazy, conflict-driven derivation of entailments. You don't compute the closure; you derive one entailed no-good exactly where the search trips, record it, continue.
P×Csets how many you derive. So the "deducible-but-not-derived" gap is filled, lazily, by the no-goods you learn.
It is also the provenance that prevents drift
The no-good store = the collapse-history = provenance (round-tree-flight-recorder). Without it → you re-walk worlds already collapsed = the "world-wandering" of drift-is-world-wandering. "Record collapses or you can't converge" = "keep provenance or you drift" — the same thing.
One line
Dead end → analyze the conflict → backjump to the real culprit (maybe in another sub-tree) + learn a no-good into C. The assignment backtracks non-monotonically, but learned collapse-info grows monotonically — that's what guarantees convergence; and it doubles as the lazy solution to deducible≠known and as the provenance that prevents drift.