The seam to an external solver (ultimately an ASP/clingo backend) for assigning truth at the edges — the defeasible nodes that a set of soft, prioritized contradictions leaves genuinely undecided.
Design constraints (see docs/nmtms.md):
Most of the KB is monotonic / default-true with no conflict; only the edges are contested, so a Program covers just the contested defeasible nodes.
Known-true content (:monotonic) is never sent — it is the fixed background the solver assumes, not something it decides.
Contradictions are soft and prioritized: a solve never fails. Instead the solver reports which contradictions it could not satisfy (their sentences are the result), highest priority first.
A solve is order-independent. Which side of a tie loses may not depend on
when anything was asserted — see content-key. This is the engine-wide
invariant (docs/nmtms.md): the same knowledge, given in any order, must yield
the same beliefs.
A Program is a self-contained description a real backend renders to ASP. This
namespace ships only a deterministic local stub solver; a real backend is a
future plug-in registered with core/set-solver.
The seam to an external solver (ultimately an ASP/clingo backend) for assigning truth at the *edges* — the defeasible nodes that a set of soft, prioritized contradictions leaves genuinely undecided. Design constraints (see docs/nmtms.md): * Most of the KB is monotonic / default-true with no conflict; only the edges are contested, so a Program covers just the contested defeasible nodes. * Known-true content (:monotonic) is never sent — it is the fixed background the solver assumes, not something it decides. * Contradictions are *soft and prioritized*: a solve never fails. Instead the solver reports which contradictions it could not satisfy (their sentences are the result), highest priority first. * **A solve is order-independent.** Which side of a tie loses may not depend on when anything was asserted — see `content-key`. This is the engine-wide invariant (docs/nmtms.md): the same knowledge, given in any order, must yield the same beliefs. A `Program` is a self-contained description a real backend renders to ASP. This namespace ships only a deterministic local *stub* solver; a real backend is a future plug-in registered with `core/set-solver`.
(content-key program handle)A stable total order on contested assumptions, derived from what they assert.
Handles are allocated in assertion order, so ordering by handle makes the outcome of a tie depend on the order the knowledge arrived — the Nixon diamond would elect the pacifist or the non-pacifist purely according to which was typed first. That is the order-dependence this exists to remove: the content of a sentex is the same whenever it is asserted, so a content-keyed choice is stable.
The choice it produces is still arbitrary — two equally-specific defaults give no principled winner, and a real ASP backend would enumerate both answer sets. Arbitrary but stable is the contract; arbitrary and order-dependent is a bug.
A stable total order on contested assumptions, derived from **what they assert**. Handles are allocated in assertion order, so ordering by handle makes the outcome of a tie depend on the order the knowledge arrived — the Nixon diamond would elect the pacifist or the non-pacifist purely according to which was typed first. That is the order-dependence this exists to remove: the content of a sentex is the same whenever it is asserted, so a content-keyed choice is stable. The choice it produces is still *arbitrary* — two equally-specific defaults give no principled winner, and a real ASP backend would enumerate both answer sets. Arbitrary but stable is the contract; arbitrary and order-dependent is a bug.
A deterministic stub standing in for a real answer-set solver: satisfy
contradictions highest-priority first by defeating the contested member with the
greatest content-key; a contradiction none of whose live members is contested is
unsatisfiable and is reported as violated. A real ASP backend replaces this
without touching callers.
Greedy, one contradiction at a time — it does not optimize globally, so two
overlapping pairs can cost two defeats where a real backend would spend one on
the shared member (docs/nmtms.md). What it must not do is spend a defeat on a
nogood that is already satisfied; see the first cond branch.
A deterministic stub standing in for a real answer-set solver: satisfy contradictions highest-priority first by defeating the contested member with the greatest `content-key`; a contradiction none of whose live members is contested is unsatisfiable and is reported as violated. A real ASP backend replaces this without touching callers. Greedy, one contradiction at a time — it does not optimize globally, so two overlapping *pairs* can cost two defeats where a real backend would spend one on the shared member (docs/nmtms.md). What it must not do is spend a defeat on a nogood that is already satisfied; see the first `cond` branch.
(nogood-members ng)Every handle a nogood involves — its positive members (:nogood, forbidden to hold
together) and its negated members (:neg, forbidden to be absent together, e.g. an
at-least-one requirement). :neg is optional and usually absent.
Every handle a nogood involves — its positive members (`:nogood`, forbidden to hold together) and its negated members (`:neg`, forbidden to be *absent* together, e.g. an at-least-one requirement). `:neg` is optional and usually absent.
(program contested nogoods content)Build a solver Program for a set of contested handles and the nogoods among
them. Contradiction members that are not contested are fixed — known-true
background that is assumed, never decided.
content maps each contested handle to what it asserts. A solver needs it to
break ties on what a datum says rather than on its handle; a real ASP backend
needs it to name atoms stably across runs.
Build a solver Program for a set of `contested` handles and the `nogoods` among them. Contradiction members that are not contested are `fixed` — known-true background that is assumed, never decided. `content` maps each contested handle to what it asserts. A solver needs it to break ties on *what a datum says* rather than on its handle; a real ASP backend needs it to name atoms stably across runs.
(solve solver program)Assign truth to program's contested assumptions. Return
{:defeat #{handle ...} ; assumptions to disbelieve
:violated [nogood ...]} ; contradictions left unsatisfiable (the result)
Assign truth to `program`'s contested assumptions. Return
{:defeat #{handle ...} ; assumptions to disbelieve
:violated [nogood ...]} ; contradictions left unsatisfiable (the result)cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |