Chapter 12 – Assumption-Based Truth Maintenance Systems (ATMS)

One belief engine that reasons in all contexts at once: instead of holding a single set of beliefs and revising it, it labels every fact with the assumption-sets under which it holds. companion index

The big idea

Every TMS we have built so far – the JTMS and the LTMS – maintains one belief state at a time. You assume some premises, propagate, and read off what is currently believed. To explore a different set of assumptions you change your mind: retract a premise, let the consequences un-derive, assume something else, propagate again. That is the whole point of dependency-directed backtracking – it makes switching contexts cheap.

The ATMS asks a more radical question: why hold only one context at a time? A diagnosis or design problem often has many candidate worlds, and the expensive part is the shared inference common to all of them. If you keep flipping between contexts, you keep re-deriving the same conclusions.

The ATMS’s answer is to compute, for every fact, the complete set of assumption-combinations under which that fact is true, all at once and shared. You never “switch contexts.” You ask a fact which contexts it holds in, and the answer is sitting right there attached to it. The data structure that holds that answer is the label.

Two slogans capture the difference:

  • A JTMS/LTMS is a single-context engine: “given these assumptions, what do I believe?”
  • An ATMS is a multi-context engine: “for every fact, under exactly which assumption-sets is it believed?”

The price is that labels can grow exponentially (we will see exactly when and why). The payoff is that shared sub-derivations are computed once and reused across all contexts – which is precisely the situation in diagnosis, qualitative reasoning, and interpretation problems where the ATMS shines.

Scope note. This chapter’s system is not implemented in this Python package – we built the JTMS/LTMS family, not the ATMS. So this page is a conceptual walkthrough, and “Try it in this repo” points at the closest machinery we do have (dependency-directed search and prime-implicate completion) plus the conceptual exercise analysis in ../exercises/ch12/.

Concepts, step by step

Five pieces of vocabulary do all the work. Get these and the rest follows.

Assumptions

An assumption is a special node you are allowed to believe freely – a premise you can switch on or off without justification. In a diagnosis problem, “component C is working normally” is an assumption; in interpretation construction, “this observation is explained by hypothesis H” is an assumption. Assumptions are the atoms out of which contexts are built.

Environments

An environment is just a set of assumptions. It denotes their conjunction: the environment {A, B} means “assume A and B both hold.” An environment is the ATMS’s word for a context. The empty environment {} is the context that assumes nothing (only the unconditional facts hold there).

Environments form a lattice ordered by subset: {A} is “weaker / more general” than {A, B} because it commits to less.

Labels (the heart of the ATMS)

The label of a node n is a set of environments {E1, ..., Ek}. It means exactly: n is true in any context that includes (a superset of) one of these environments. Each Ei is one independent way to derive n from assumptions.

A correct ATMS keeps every label satisfying four label properties at all times:

Property What it guarantees
Sound Every environment in the label really does entail n.
Complete Every consistent environment that entails n is covered by (a superset of) some label environment.
Minimal No label environment is a superset of another in the same label.
Consistent No label environment is a nogood (see below).

Minimality is what keeps labels from drowning in redundancy: if {A} already gives you n, there is no point also listing {A, B} – it is subsumed. So you keep only the most general derivations.

Justifications

A justification is a Horn-like rule, a1 & a2 & ... & ak => c: a conjunction of antecedents implies a consequent. This is the same shape as a JTMS justification. The ATMS’s job is to turn justifications plus assumptions into correct labels.

The label-propagation rule is the one computation that matters. To push a label through x & y => c, you form the pairwise cross-product of label(x) and label(y):

for each Ex in label(x):
    for each Ey in label(y):
        E = Ex ∪ Ey            # union the assumption sets
        if E is consistent:    # not a superset of any nogood
            add E to a candidate set
prune the candidate set: drop any E that is a superset of another (minimality)
merge what survives into label(c)

Because set union is associative and commutative, it does not matter whether you combine three antecedents all at once or two at a time – you get the same final minimal label. (Exercise 1 turns exactly this observation into the “chain vs. binary tree of justifications” result.)

Nogoods

A nogood is an environment that is inconsistent – a combination of assumptions that leads to a contradiction. Once you discover a nogood, two things follow for free:

  • Any superset of a nogood is also inconsistent (nogoods are upward-closed), so you can prune whole families of environments at once.
  • Every label must avoid nogoods (the consistency property). When a new nogood is found, the ATMS must walk existing labels and remove any environment that the nogood now rules out.

Nogoods are how the ATMS keeps labels small in practice: a problem with lots of mutual exclusion (no two queens on the same row, no two adjacent regions the same color) generates many nogoods, and each one prunes the search space.

Putting it together: an ATMS query

Once labels are computed, queries are cheap set operations, not new inference:

  • Is n true in environment E? -> does some environment in label(n) satisfy E' ⊆ E?
  • Is E consistent? -> is E not a superset of any nogood?
  • What follows in context E? -> every node whose label contains a subset of E.

That is the whole magic: the hard work happens once, at label-construction time, and every context query is then a lookup.

Why this is “a JTMS run in all contexts at once”

Here is the cleanest way to understand the ATMS, and it is also Exercise 2. Imagine taking a JTMS and running it on the powerset of assumptions: for every subset E, enable exactly those assumptions, propagate to quiescence, and for each fact the JTMS now believes, record E in that fact’s growing label. Drop the inconsistent subsets as nogoods; minimize each collected set at the end. You would get exactly the ATMS labels.

That construction is correct but takes 2^A JTMS runs for A assumptions. The real ATMS computes the identical labels in one incremental pass by combining labels symbolically (the cross-product rule) instead of enumerating models. The ATMS is the JTMS run in all contexts at once, done efficiently.

The fundamental cost: exponential labels

Symbolic combination is clever, but it cannot beat an exponential answer. If the problem is genuinely disjunctive, the minimal label is genuinely exponential, and no implementation trick avoids it. Exercise 3 makes this concrete: n independent two-way choices (Ai => xi, Bi => xi) feeding one conjunction x1 & ... & xn => GOAL gives

label(GOAL) = { {y1, ..., yn} : each yi ∈ {Ai, Bi} }   ->   2^n environments

from only 2n + 1 justifications. This is the cost of completeness. Where the JTMS pays for context-switching, the ATMS pays for keeping all contexts alive. Nogoods are the relief valve: they prune the combinations that turn out inconsistent, which is why real problem solvers (diagnosis, CSPs) stay tractable.

Interpretation construction

The ATMS by itself just maintains labels. To solve a problem you drive it with interpretation construction: a dependency-directed search that grows candidate environments by combining choice sets, pruning with the nogood database. This is the ATMS analogue of the LTRE’s dependency-directed search in dds.py.

The recurring problem is the interpretation bulge: the intermediate set of partial environments can balloon long before the search finishes. The cures are the standard CSP toolkit, transplanted onto labels:

  • Filtering (Exercise 4): apply an expensive solution constraint lazily, only when the candidate set crosses a size threshold (and once at the end so the answer stays correct).
  • Forward checking + dynamic reordering (Exercise 8): after each choice, delete now-inconsistent choices from future choice sets, and always expand the choice set with the fewest live choices left (minimum-remaining-values / fail-first).

The examples, explained

The chapter’s worked examples are about seeing labels form and shrink. The package does not run them, but here is what each one is teaching.

  • A node’s label as a set of supports. The running figure (the book’s Figure 12.6 family) shows a GOAL node whose label is built up by propagating through a network of justifications. The lesson: the label is not one support, it is every minimal support, and it is recomputed incrementally as justifications are added. Exercise 1 re-derives the same label two ways (one big justification vs. a balanced binary tree of pairwise ones) to show the label is invariant to how you arrange the combination.

  • Nogoods pruning a label. When a contradiction marks an environment as a nogood, the ATMS sweeps labels and removes every environment that is now a superset of it. The example shows a label shrinking as constraints arrive – the opposite of monotone forward chaining, and exactly the behavior that lets the ATMS represent “this fact holds, but not in the worlds we have ruled out.”

  • The cross-product blow-up. The exponential-label example (mirrored in Exercise 3) shows disjunctive structure forcing the label of a conjunction to be the full product of its antecedents’ labels. It is the concrete picture behind “completeness is exponential,” and the motivation for nogoods and filtering.

  • Interpretation construction as search. The N-queens / CSP examples show the ATMS used as a solver: each column or variable is a choice set, attacking pairs are nogoods, and interpretation construction enumerates the consistent environments. This is the same problem shape the LTRE solves with DD-search in coloring_dds.py – a good thing to run as a stand-in (see below).

Exercises walk-through

The ATMS is out of package scope, so the ../exercises/ch12/ solutions are conceptual: algorithm sketches, derivations, and complexity arguments rather than runnable code. There is no solutions.py here. The notable results:

  • Ex 1 (label invariance). A chain justification n1 & ... & n8 => GOAL and a balanced binary tree of pairwise justifications produce the same label, because the cross-product’s set-union is associative and commutative. The tree is cheaper per step (two labels at a time), shares sub-results, and is more incremental (O(log k) nodes to recompute on a change); the cost is more auxiliary nodes to store and maintain.

  • Ex 2 (simulate ATMS with a JTMS). Enumerate the powerset of assumptions; for each subset run the JTMS, record nogoods for the inconsistent ones, add the subset to the label of every believed node, then minimize. Correct but 2^A propagations – the exercise’s whole point is that the ATMS gets the same answer in one symbolic pass.

  • Ex 3 (exponential labels). The Ai => xi, Bi => xi, x1 & ... & xn => GOAL family forces 2^n minimal environments from 2n + 1 justifications. Disjunctive structure means exponential labels, period.

  • Ex 4 (filtering). A filter(E) predicate applied lazily when the candidate set bulges (and once at the end for soundness); rewritten N-queens drops the pre-installed attack nogoods and instead culls attacking boards when the set swells. Eager pairwise nogoods win for cheap constraints; lazy filtering wins for expensive or global ones.

  • Ex 5 (bit-vector environments). Encode each assumption as a bit index; environments become integers. Union is OR, subset test is (a AND b) == a, consistency is a handful of AND/compares against nogoods – O(1) for up to a word’s worth of assumptions, with the caveat that bit vectors waste space when assumptions are many but environments are sparse.

  • Ex 6 (spatial planning, open project). Represent rooms/floors as an adjacency graph with a metric; encode hard constraints (capacity, exclusivity) as nogoods and soft preferences (near/far/needs/contiguous) as an additive objective; solve with interpretation construction plus branch-and-bound filtering (Ex 4) to control the bulge; output ranked, explained solutions.

  • Ex 7 (clausal ATMS). Accepting arbitrary clauses (not just Horn justifications) makes label propagation incomplete for the same reason BCP is incomplete in the LTMS: some consequences need resolution, not unit propagation. Full logical completeness requires computing prime implicates – the same machinery our cltms.py uses for the LTMS, and the same exponential wall.

  • Ex 8 (forward checking + reordering). Interpretation construction with the nogood database as a consistency oracle: after committing a choice, prune now-inconsistent future choices; always expand the smallest remaining choice set. Search-order optimizations only – they change speed, not which interpretations exist.

  • Ex 9 (a CSP solver + two colorings). Variables as choice sets, allowed tuples as the only legal pairs (anything unlisted is a nogood). The two graph-coloring instances are the punchline: a triangle (K3) is 3-colorable with 3! = 6 solutions; K4 needs four colors, so 3-coloring it has no solution (every full attempt collapses to a nogood and the interpretation set is empty).

Try it in this repo

The ATMS itself is not implemented here. What you can run are the pieces this package shares conceptually with the ATMS, plus the conceptual analysis in the exercises folder.

The closest behavioral analogue is dependency-directed search in the LTRE, which (like ATMS interpretation construction) assigns choice sets and learns nogoods to prune dead ends:

. .venv/bin/activate
python examples/coloring_dds.py      # graph coloring by DD-search: choice sets + nogoods
python exercises/ch10/solutions.py   # N-queens via DD-search (counts 4->2, 5->10, 6->4)

The map-coloring demo is the same problem shape as ATMS interpretation construction: each region is a choice set, each “adjacent regions, same color” fact is a nogood, and the search enumerates the consistent assignments – exactly what the ATMS does with environments and labels, but holding one context at a time instead of all at once. The relevant code is dds.py.

The other shared idea is prime-implicate completion, which Exercise 7 identifies as the road to a clausal ATMS. Our LTMS gains completeness the same way the chapter describes for an arbitrary-clause ATMS:

from ltms.core import LTMS
from ltms.cltms import complete
m = LTMS()
x, y = m.create_node("x"), m.create_node("y")
m.add_clause([x], [y], "x v ~y")   # (x ∨ ¬y)
m.add_clause([x, y], [], "x v y")   # (x ∨ y)   -- together entail x, but BCP misses it
assert not x.is_known               # unit propagation alone is incomplete
complete(m)                         # add prime implicates by resolution
assert x.is_true                    # now forced

That complete() step – resolution to a fixpoint – is precisely the prime-implicate machinery a clausal ATMS would graft onto the environment/label layer (see cltms.py and ch13).

For the ATMS-specific reasoning (labels, environments, the cross-product rule, the exponential family, the filtered/forward-checking solvers, the CSP colorings), the worked analysis lives in ../exercises/ch12/README.md.

Takeaways

  • The ATMS is a multi-context belief engine: instead of one belief state it attaches every fact a label – the set of minimal, consistent environments under which the fact holds.
  • The five primitives are assumptions, environments (sets of assumptions), labels (sets of environments), justifications (Horn rules), and nogoods (inconsistent environments).
  • Labels are kept sound, complete, minimal, and consistent; propagation through x & y => c is the pairwise cross-product of labels, pruned by minimality and nogoods.
  • Conceptually it is a JTMS run in every context at once, done by combining labels symbolically rather than enumerating the 2^A contexts.
  • The cost is that disjunctive structure forces exponential labels; nogoods, filtering, and forward checking are how interpretation construction stays tractable in practice.
  • Extending the ATMS to arbitrary clauses runs into the same completeness wall as BCP – it needs prime implicates, the trick our cltms.py uses for the LTMS.

Back to the companion index · previous: Chapter 11 · next: Chapter 13 – CLTMS.

This site uses Just the Docs, a documentation theme for Jekyll.