Chapter 16 – Assumption-Based Constraint Languages

Taking the constraint propagator of chapter 15 and giving it the power to reason in many hypothetical worlds at once, by hanging it on an ATMS instead of a single-context TMS. companion index

The big idea

Chapter 15 built TCON, an antecedent constraint language: a network of cells (variables that hold at most one value) wired together by constraints (devices like adder, multiplier, relay). When enough of a constraint’s cells have values, a small antecedent rule fires, computes a value for another cell, and records which cells it read as that value’s antecedents. Because every value remembers its support, the system can explain a result and retract it when a premise goes away.

That is already useful, but it has one current value per cell. The moment you want to ask “what would the network compute if I assumed switch = on?” and then “what about switch = off?”, plain TCON has to change the cell, re-run the affected rules, and on a context switch undo and redo large amounts of propagation. Each context is paid for again.

Chapter 16 asks: what is the right truth-maintenance substrate for a constraint language that does a lot of hypothetical reasoning? It answers by building three versions of the same propagator and comparing them:

TCON — no TMS; values are just stored, contexts cost re-execution.
TCON + JTMS — each value is a JTMS node with a justification; switching contexts is belief propagation rather than re-execution, but each node still holds a single current label, so a value that is true here and false there must be relabelled when you move.
ATCON (TCON + ATMS) — each value is an ATMS node whose label is the set of minimal environments (assumption sets) in which it holds. A rule fires once per distinct combination of antecedent values, and the result is recorded with the environment(s) that make it valid. There is no context switch at all: to read a cell in some context you just find the node whose label environment is a subset of that context.

The slogan from the rest of the book still applies: separate what you believe from why you believe it. The ATMS pushes that idea to its limit by maintaining all the consistent worlds simultaneously, so the constraint propagator never has to pick one.

A note on this chapter and this repo. TCON, the JTMS-backed propagator, and ATCON are not implemented in this package — porting the ATMS/constraint suite is an explicit non-goal (see BRIEFING.md). So this page is conceptual. Where it helps, it points at the closest available machinery in the repo (the LTMS/LTRE and its dependency-directed search), and the exercise analysis lives in ../exercises/ch16/.

Concepts, step by step

Cells, constraints, and antecedent rules (recap from chapter 15)

A cell holds at most one value plus a record of why. A constraint (say an adder with cells a, b, sum) is a bundle of constraint rules: tiny antecedent rules of the form “if these input cells are known, compute that output cell.” An adder has three:

a, b known → sum := a + b
sum, a known → b := sum - a
sum, b known → a := sum - b

Each rule lists exactly the cells it read as the new value’s antecedents. That discipline is the whole point: it is what lets the underlying TMS retract correctly when a premise changes. Any two of the three cells determine the third, so a constraint is multi-directional, not a one-way function.

What changes when you put a TMS underneath

The constraint machinery (cells, devices, rules) is unchanged across all three designs. What changes is where a value lives and what happens on a context switch:

	a value is…	switch contexts by…	rule fires…	re-derives a known conflict?
TCON	stored in the cell	undo + redo propagation	once per context	yes, every time
TCON + JTMS	a JTMS node + justification	belief (re)propagation	once, cached per node	possibly (single-context label)
ATCON	an ATMS node + environment label	no switch — read by subset	once per antecedent combo	never

The ATMS notions you need

Assumption — a primitive choice you can turn on or off (switch = on).
Environment — a set of assumptions, i.e. a hypothetical world.
Label — for each datum, the set of minimal environments in which it holds. “Minimal” because if a value holds in {A} there is no point recording that it also holds in {A, B}; the superset is implied.
Nogood — an environment known to be inconsistent. The ATMS keeps these and never puts an inconsistent environment into any label, so it never wastes work believing something in a dead world.

Reading a cell in a context C (itself an environment) is then a pure lookup: find the cell’s node whose label contains some environment E ⊆ C. Because labels are kept minimal and consistent, that node is unique — no propagation, no undo.

The `atcon-delay` flag (the chapter’s tuning knob)

ATCON normally runs with delay = t. In that mode, before actually executing a constraint rule, it checks whether the rule’s result could possibly be useful:

does each antecedent have external support (support coming from outside this very constraint), and
is there a single consistent environment in which all the antecedents hold at once?

If not, the rule is requeued/suppressed instead of run. These checks are has-external-support and has-complete-external-support. With delay = nil, ATCON skips the checks and fires every queued rule immediately.

The subtle part: the delay machinery itself costs effort — it computes prospective labels and hunts for a consistent witness environment. So turning delay on is a bet. It only pays off when the rule work it avoids is more expensive than the checks it adds. Exercise 1 is exactly about characterizing when that bet wins.

Why ATCON never re-derives a conflict (and TCON does)

This is the deepest structural point of the chapter. Because the ATMS stores nogoods as part of label maintenance and never context-switches, it computes each value-in-each-environment once and caches it forever. A plain TCON, by contrast, re-runs propagation per context, so it can rediscover the same small inconsistency over and over inside many different larger contexts. Exercise 2 makes that gap quantitative: it is the difference between exponential and polynomial work on a network with a small “core” conflict and a large irrelevant “tail.”

The examples, explained

The chapter’s worked material is a comparison, not a single demo: it takes the same constraint networks and runs them under each substrate to expose the trade-offs.

The same adder chain, three ways. A deterministic chain x0 = 1, x_{i+1} = x_i + 1 realized by adders shows the costs lining up. TCON recomputes the chain whenever you change x0; the JTMS version caches node values but still re-labels on a context switch; ATCON computes each value once, labels it with the single environment that holds, and answers any context by subset lookup. With one consistent world and cheap rules, the example also exposes that delay = t here is pure overhead (see exercise 1a/1b) — every rule’s result is wanted, so the up-front “is this useful?” check never prevents a single firing.
A network with mutually inconsistent assumptions. Flip the flavor: wire a constraint whose output feeds back into its own siblings’ inputs, and add assumptions that are pairwise inconsistent. Now many antecedent combinations exist node-by-node, but no single consistent environment holds a whole antecedent set. This is the regime where delay = t earns its keep: has-complete-external-support discovers up front that there is no consistent witness, and the expensive rule body never runs. Run the same network with delay = nil and every doomed combination executes, produces a value the ATMS immediately labels with a nogood (useless), and the work is thrown away — an exponential pile of wasted expensive firings (exercise 1c).
The small-core / large-tail network. Two choice cells a, b whose combination a = T, b = T propagates to a contradiction, plus k completely unrelated Boolean choice cells d1 … dk. Read under TCON it shows the conflict being re-derived once per tail setting (2^k times); read under ATCON (or a JTMS with a nogood table) it shows the conflict recorded once and pruned by superset thereafter. This is the example exercise 2 turns into a proof of an exponential speedup.

The throughline: the constraint program is identical in every case; only the truth-maintenance substrate underneath changes, and that change alone moves the asymptotics.

Exercises walk-through

Full paraphrased statements and original analysis (analysis-only, no runnable code) are in ../exercises/ch16/README.md.

Exercise 1 (★) — when `atcon-delay nil` beats `t`, and vice versa

The task is to exhibit one program that is clearly faster with delay off and one that is clearly worse with delay on, then state the general rule. The solution frames the whole thing as a wager on a single inequality:

savings = (number of useless rule firings prevented) × (cost per rule) versus overhead = (number of rules considered) × (cost of one delay check).

delay = t wins exactly when savings > overhead. The two ends of the spectrum:

delay = nil wins when rules are cheap and almost every firing is useful — deterministic, low-branching, contradiction-free networks (the adder chain). The check computes a prospective label and searches for a witness n times and never stops a single rule, so its cost is pure waste that grows linearly with the network.
delay = t wins when rules are expensive and many candidate firings are useless — networks with feedback inside constraints and many mutually inconsistent assumptions, so lots of antecedent combinations have no consistent witness environment. A cheap up-front label computation then saves a costly body, possibly an exponential number of times.

The solution also flags an important methodological caveat: if rules have side effects or signal contradictions, the order of firing differs between the two modes, so a fair timing comparison must be made on a side-effect-free, confluent network. (The book makes the same point.)

Exercise 2 (★★) — an explicit nogood database for an exponential JTMS speedup

Assume the JTMS keeps an explicit table of nogoods (assumption sets already known inconsistent), consulted before any assumption is enabled. The task is a TCON program whose running time drops from exponential to polynomial because of that table.

The construction is the small-core / large-tail network: a two-cell conflict {a = T, b = T} plus k irrelevant choice cells d1 … dk, giving 4 × 2^k candidate contexts.

Without the nogood database, search fixes a = T, b = T, then iterates over all 2^k tail settings, re-deriving the same a ∧ b contradiction every time — nothing remembers it is already dead. Work is Θ(2^k) wasted re-derivations.
With the database, the first time a = T, b = T is enabled the contradiction is derived and the minimal nogood {a = T, b = T} is recorded. On every later context, the pre-enable check sees that the context supersets a recorded nogood and prunes the entire branch before enabling and before touching the tail. Work collapses to O(k).

The solution makes the punchline explicit: this is exactly dependency-directed backtracking with nogood caching — generalize a refuted reason to the small set of choices that actually caused the conflict, then prune every future context containing that set. It is also the JTMS recovering, by hand, the conflict-caching the ATMS gets for free: the ATMS stores nogoods as part of label maintenance and never re-derives a known conflict, so bolting an explicit nogood table onto a JTMS-backed TCON buys back the key asymptotic win without paying for full ATMS label machinery. (The price the JTMS still pays: it re-executes rules across genuinely distinct consistent contexts, which ATCON would also cache.)

Ex	Topic	Core result
1 (★)	`atcon-delay` t vs nil	The flag is a wager: `delay=t` wins when rules are expensive and many firings are useless; `delay=nil` wins when rules are cheap and almost every firing is useful.
2 (★★)	Explicit nogood DB in JTMS-TCON	Small-core/large-tail program goes Θ(2^k) → O(k); recovers ATMS-style conflict caching without full label machinery.

Try it in this repo

ATCON itself is not in this package, so there is nothing to run for the constraint language directly. The closest runnable machinery is the LTMS/LTRE, which shares the two ideas this chapter turns on:

Nogood-caching, dependency-directed backtracking is implemented in src/ltms/dds.py. When assuming a choice causes a contradiction, a pushed handler finds the assumptions actually responsible (via assumptions_of_clause) and installs a nogood that forbids that exact combination — so the same dead branch is never re-explored. This is precisely the “record the conflict once, prune by superset thereafter” mechanism that exercise 2 relies on, just over clauses rather than over constraint cells.
Well-founded support and clean retraction — every forced value in the LTMS keeps the clause that forced it, so retracting a premise un-derives its consequences. That is the single-context analogue of a value remembering its antecedents in a constraint cell.

. .venv/bin/activate
python examples/coloring_dds.py          # dependency-directed search learning nogoods
python exercises/ch10/solutions.py       # N-queens via DD-search (nogood per attacking pair)

A minimal taste of the learning-once-and-pruning idea in Python, using the dependency-directed search that backs the constraint reasoning above:

from ltms.ltre import LTRE
from ltms.dds import dd_search

e = LTRE()
# ... install constraints as clauses, then search choice sets ...
# dd_search assumes each choice, runs rules, and on a contradiction records a
# nogood so the same dead combination is pruned everywhere after.
solutions = dd_search(e, choice_sets=[...], extract=lambda eng: ...)

For the actual chapter-16 analysis (the atcon-delay characterization and the exponential nogood-database argument), read ../exercises/ch16/README.md — it is conceptual, with codeRuns = false and no solutions.py, by design.

If you want to see the multi-context idea that ATCON inherits, the ATMS itself is covered as a concept chapter (see the companion index entries for chapters 12 and 14); ATCON is “the ATMS, wired into a constraint propagator.”

Takeaways

A constraint language can ride on any truth-maintenance substrate; the cells, devices, and rules don’t change — only what a value is and what a context switch costs changes.
TCON re-executes per context, TCON + JTMS caches node values but keeps a single-context label, and ATCON stores each value’s set of minimal consistent environments and so needs no context switch at all — you read a cell by subset lookup.
ATCON’s superpower is that it never re-derives a known conflict, because the ATMS keeps nogoods and never labels anything in a dead world.
The atcon-delay flag is a bet: the up-front “could this rule possibly matter?” check pays only when rules are expensive and many firings are doomed; on cheap, deterministic, single-world networks it is pure overhead.
You can recover most of ATCON’s asymptotic win on a cheaper JTMS by adding an explicit nogood database consulted before enabling assumptions — turning “rediscover the conflict in every context” into “record it once, prune by superset.” That mechanism is implemented for clauses in src/ltms/dds.py.

Back to the companion index · previous: Chapter 15 — Antecedent Constraint Languages · next: Chapter 17 — A Tiny Diagnosis Engine. </content> </invoke>