Chapter 9 — Logic-Based Truth Maintenance Systems (LTMS)

The heart of this project: belief over propositional clauses, maintained by Boolean Constraint Propagation. companion index

The big idea

A justification-based TMS (chapters 6–7) records beliefs as definite rules: “these antecedents being IN make this consequent IN.” That is enough for forward chaining, but it cannot say a proposition is false, and it cannot reason with disjunctions (“either the bulb is dead or there is no power”).

The LTMS fixes both by changing the representation. Instead of in/out, a node carries a three-valued label — TRUE, FALSE, or UNKNOWN — so negation is just the label, with no separate node for not P. And instead of definite justifications, the engine stores arbitrary clauses (disjunctions of signed literals). Propagation over clauses is Boolean Constraint Propagation (BCP), which is exactly the unit propagation at the heart of every SAT solver: whenever a clause has only one way left to be satisfied, take it.

The result is a small, explainable, incrementally-revisable belief engine that is sound but not complete — a trade we make on purpose (more below).

In this repo the engine is src/ltms/core.py, with a second, SAT-style implementation in src/ltms/watched.py.

Concepts, step by step

Nodes, literals, clauses

  • A node (TmsNode) is one proposition. Its label is TRUE/FALSE/UNKNOWN; its support records why it has that label.
  • A literal is a (node, sign) pair — (p, TRUE) means “p”, (p, FALSE) means “not p”. A literal is satisfied when the node’s label equals the sign, violated when it equals the opposite, and unknown otherwise.
  • A clause (Clause) is a list of literals meaning their disjunction. The clause (p ∨ ¬q) is [(p, TRUE), (q, FALSE)].

The counter trick (why BCP is fast)

Naively, deciding whether a clause is “unit” (one way left) means scanning its literals every time a node changes. BCP avoids that with two counters per clause, maintained incrementally:

  • sats = how many literals currently satisfy the clause.
  • pvs (“potential violators”) = how many literals are not yet violated, i.e. #unknown + #satisfying.

From these, the clause’s state is O(1):

condition meaning
pvs == 0 violated (every literal false → contradiction)
pvs == 1 unit (one way left → force it)
sats > 0 satisfied

When a node is labelled TRUE, the engine touches only the clauses that mention it: clauses where it appears positively gain a satisfier (sats += 1); clauses where it appears negatively lose a potential violator (pvs -= 1). When pvs drops below 2, the clause is queued for checking. This is set_truth in core.py.

A subtlety worth internalizing: a satisfying literal still counts toward pvs. Why? Because if the assumption that satisfied it is later retracted, the literal could become a violator again. That is also why satisfied clauses are never thrown away — their counters must stay live for correct retraction.

Boolean Constraint Propagation

The loop (_run_bcp → _check_clause) drains a work-list of clauses:

  • if a clause is violated, record it (do not raise — see below);
  • if it is unit, find the lone unknown literal and set_truth it to its sign, recording the clause as that node’s well-founded support;
  • otherwise leave it.

Forcing a node may make other clauses unit, so the loop continues to a fixpoint.

Deferred contradictions

BCP must not throw the instant it sees a violated clause. The counters are mid-update during propagation; bailing out would leave them inconsistent and corrupt a later retraction. Instead, violated clauses are collected, and only at the end of the top-level operation does check_for_contradictions dispatch them to the handler stack. A handler returns truthy if it resolved the conflict; the default behavior, with no handler, is to raise LTMSContradiction.

Assumptions, nogoods, and dependency-directed backtracking

A premise is just a unit clause. An assumption is a node you choose to believe and can later withdraw; its support is the sentinel ENABLED_ASSUMPTION. When a contradiction implicates assumptions, the avoid_all handler:

  1. finds the assumptions underlying the violated clause (assumptions_of_clause),
  2. retracts a culprit, and
  3. installs a nogood — a clause forbidding that exact assumption combination —

so the same dead end is never revisited. That is dependency-directed backtracking, and the nogood is a learned clause (the same idea CDCL SAT solvers call clause learning).

Two-phase retraction

Withdrawing an assumption is the delicate operation. It is strictly two phases:

  1. propagate_unknownness — set the assumption, and everything it transitively forced, back to UNKNOWN, undoing their counter effects.
  2. find_alternative_support — only after phase 1, re-run BCP on the freed nodes’ clauses to see if some other clause can re-derive them.

Doing the search eagerly (per node, during phase 1) would let two nodes prop each other up with no real ground — ill-founded circular support. The split is what keeps belief well-founded.

Soundness, not completeness

BCP is unit resolution only, so it is deliberately incomplete:

  • Literal-incomplete: {x ∨ ¬y, x ∨ y} entails x, but neither clause is ever unit, so x stays UNKNOWN.
  • Refutation-incomplete: the four-clause set {¬x∨¬y, ¬x∨y, x∨¬y, x∨y} is unsatisfiable, yet every clause keeps two potential violators, so BCP detects nothing.

This is the right default — most problem solvers tolerate it and it keeps propagation cheap. Chapter 13 shows how to recover completeness on demand by adding prime implicates (ch13).

Watched literals

The counter scheme touches every clause of an assigned node. The SAT-solver alternative is two watched literals per clause: a clause is only re-examined when one of its two watched (non-false) literals becomes false, at which point we look for a replacement; if none exists the other watched literal is forced or the clause is in conflict. watched.py implements this and is verified to produce the same forced labels and contradictions as the counter engine (a differential test) and to agree with the MiniSat SAT solver.

The examples, explained

  • Unit propagation. Assert (a ∨ b) (nothing forced — two potential violators). Then assert ¬a; now the clause is unit and b is forced TRUE, with the clause recorded as b’s support.
  • Implication chains. p → q is the clause (¬p ∨ q). Asserting p forces q, then q → r forces r — a chain of single BCP steps, each with explicit support so the whole derivation can be explained or retracted.
  • A contradiction. Assert p, then assert ¬p: the second unit clause is immediately violated and (with no handler) raises.
  • Belief revision. Two clauses both supporting one conclusion; retract one premise and the conclusion survives on the other, retract both and it goes UNKNOWN. This is the examples/kb/belief_revision.kb story.

Exercises walk-through

Full set with paraphrased statements and answers: ../exercises/ch09/. Highlights, demonstrated in ../exercises/ch09/solutions.py:

  • Clause blow-up. Converting a big “disjunction of conjunctions” to CNF is a cross product: the clause count is the product of the disjuncts’ sizes. The book’s 13-disjunct fault model expands to ~6 million clauses — concrete motivation for chapter 13’s no-CNF techniques.
  • Taxonomy size. “Exactly one of n” becomes n(n−1)/2 + 1 clauses (one big disjunction plus a “not both” clause per pair); verified against normalize.
  • Completeness. complete() adds the prime implicates so the two incompleteness cases above are resolved — x gets forced, and the 4-clause set is detected as unsatisfiable.
  • Switchable clauses, fixed vs. variable labels, GC of satisfied clauses — answered via the guard-node trick and assumptions_of_node (see the README).

Try it in this repo 

. .venv/bin/activate
python exercises/ch09/solutions.py                 # clause counts, taxonomy size, completeness
python examples/run_kb.py exercises/ch09/kb/incompleteness.kb   # BCP leaves x unknown
python examples/run_kb.py exercises/ch09/kb/completeness.kb     # complete() then forces x
python examples/run_kb.py exercises/ch09/kb/taxonomy.kb         # exactly-one

A minimal session in Python:

from ltms.core import LTMS, Label
m = LTMS()
a, b = m.create_node("a"), m.create_node("b")
m.add_clause([a, b], [], "a v b")   # (a ∨ b)
m.add_clause([], [a], "~a")          # ¬a  -> forces b
assert b.is_true

Takeaways

  • Negation is a label, not a node; the LTMS reasons with full clauses.
  • BCP = unit propagation, made cheap by the pvs/sats counters.
  • Every forced label keeps its well-founded support, which powers explanation, retraction, and nogood learning.
  • Contradictions are deferred then dispatched; retraction is two-phase.
  • The engine is sound, not complete — by design; recover completeness with ch13 when you need it.

Next: Chapter 10 — Putting an LTMS to Work.

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