Solving as a persistent, inert artifact: assumptionRules define choices, a
solve grounds them (scoped to a base context), enumerates the optimal answer sets,
and materializes each one as its own labeling context — a genlContext child of
the base holding the chosen truth values as inert sentexes. classify then gathers
brave/cautious over those labelings.
The two imperatives (do/label Base Into) and (do/classify Into) route here.
Belief in this KB is global (one JTMS, not an ATMS): a believed (not head) in a
context that sees the base would defeat the base's head everywhere — so only one
labeling could ever exist (the do/labeling global-commit). Materializing the truth
values inert (core/assert-inert — stored and indexed but not a JTMS premise)
sidesteps that entirely: an inert sentex is never IN, so it is invisible to the
belief-filtered nogood scan, forms no contradiction, and moves no belief. Every
answer set therefore coexists as its own context, the base KB is untouched, and the
result persists in the records for inspection.
The answer persists: the labeling contexts and the classification, as inert
sentexes in the records. The grounding — the menu of candidate choice heads —
never does. A grounding is derived solver working state, recomputable from the
assumptionRules and the base's believed facts; an inert copy would carry no
justification linking it back to what produced it, so it would rot silently the
moment the base moved. The Program keys on program-local ids (see build), and
label returns the menu as :choices for a caller who wants to see it.
And what persists is replaced on re-run, never accreted: label clears a
previous run's artifacts under the same Into before writing (see clear-run!),
and classify clears its own previous classification. Truth values from two
different groundings unioned into one context assert nothing at all.
Constraints are the engine's own contradictions among the direct ground choice
heads — a (not X)/X pair, a functional predicate given two values, or a
disjoint type clash. Choices do not propagate through ordinary rules yet
(that is provenance-propagation / full clingo grounding, the named follow-ups).
Solving as a **persistent, inert** artifact: `assumptionRules` define choices, a solve grounds them (scoped to a base context), enumerates the optimal answer sets, and materializes **each one as its own labeling context** — a `genlContext` child of the base holding the chosen truth values as inert sentexes. `classify` then gathers brave/cautious over those labelings. The two imperatives `(do/label Base Into)` and `(do/classify Into)` route here. ## Why inert, and why per-answer-set Belief in this KB is global (one JTMS, not an ATMS): a *believed* `(not head)` in a context that sees the base would defeat the base's `head` everywhere — so only one labeling could ever exist (the `do/labeling` global-commit). Materializing the truth values **inert** (`core/assert-inert` — stored and indexed but not a JTMS premise) sidesteps that entirely: an inert sentex is never IN, so it is invisible to the belief-filtered nogood scan, forms no contradiction, and moves no belief. Every answer set therefore coexists as its own context, the base KB is untouched, and the result **persists in the records** for inspection. ## What persists, and what does not The **answer** persists: the labeling contexts and the classification, as inert sentexes in the records. The **grounding** — the menu of candidate choice heads — never does. A grounding is derived solver working state, recomputable from the assumptionRules and the base's believed facts; an inert copy would carry no justification linking it back to what produced it, so it would rot silently the moment the base moved. The Program keys on program-local ids (see `build`), and `label` returns the menu as `:choices` for a caller who wants to see it. And what persists is **replaced on re-run**, never accreted: `label` clears a previous run's artifacts under the same `Into` before writing (see `clear-run!`), and `classify` clears its own previous classification. Truth values from two different groundings unioned into one context assert nothing at all. ## MVP scope (docs/solving.md) Constraints are the engine's own contradictions among the **direct** ground choice heads — a `(not X)`/`X` pair, a `functional` predicate given two values, or a `disjoint` type clash. Choices do **not** propagate through ordinary rules yet (that is provenance-propagation / full clingo grounding, the named follow-ups).
(classify kb into)Gather brave/cautious over the labelings a prior (do/label _ Into) produced, and
record the result as inert sentexes in <Into-base>ClassContext. A choice head is
(forced H) — (head) in every labeling (a cautious/skeptical consequence),(excluded H) — (not head) in every labeling,(supportable H) — otherwise (a brave/credulous consequence only).Pure aggregation over the persisted labeling contexts — no solver, no whole-KB scan,
and one extent read per labeling (polarity-table), with everything after in
memory. Its own previous classification is cleared first (replace-on-rerun,
same discipline as label): a stale classification describes labelings that no
longer exist. Returns {:class-context :forced [..] :supportable [..] :excluded [..]},
or :count 0 :reason :no-labelings when label was never run for Into.
Gather brave/cautious over the labelings a prior `(do/label _ Into)` produced, and
record the result as inert sentexes in `<Into-base>ClassContext`. A choice head is
* `(forced H)` — `(head)` in **every** labeling (a cautious/skeptical consequence),
* `(excluded H)` — `(not head)` in every labeling,
* `(supportable H)` — otherwise (a brave/credulous consequence only).
Pure aggregation over the persisted labeling contexts — no solver, no whole-KB scan,
and **one extent read per labeling** (`polarity-table`), with everything after in
memory. Its own previous classification is cleared first (replace-on-rerun,
same discipline as `label`): a stale classification describes labelings that no
longer exist. Returns `{:class-context :forced [..] :supportable [..] :excluded [..]}`,
or `:count 0` `:reason :no-labelings` when `label` was never run for `Into`.(label kb base into)(label kb base into mode)Ground the assumptionRules visible from Base (honoring their exceptWhen
guards), detect the constraints among the ground choice heads — the direct
auto-clashes and every set/hardConstraint / set/softConstraint rule's body
ground into a nogood — and solve.
mode (an optional third argument, default :all) picks how many worlds:
:all — enumerate every optimal answer set and materialize each as its own
inert labeling context: a genlContext child of Base named
<Into-base><i>Context (skipping any slot an unrelated context occupies) holding
(head) for a chosen-true choice, (not head) for a chosen-false one, and its
labelingOf ownership marker. The worlds coexist and persist for do/classify to
aggregate; base belief is untouched. This is the studying-many-worlds mode, and it
is infeasible where the optima are astronomically many (a large graph coloring has
too many valid colorings to enumerate).:one — commit to one optimal answer set via a single :label solve
(minimizing defeated assumptions — keep as much belief as possible), and return it
in the result without persisting anything. The solving mode: it wants an
answer, not an artifact, so it is feasible at scale (one solve, no enumeration, no
materialization). Into is accepted for a uniform imperative shape but unused.:sat — :one, but plain satisfaction rather than optimization: no
keep-belief objective, so clingo stops at the first model instead of proving
cost-optimality over the choice atoms. For a program whose hard constraints
already pin what must be chosen (a graph coloring's hard at-least-one), "keep as
much as possible" is redundant and the optimization is a scaling wall — :sat
finishes where :one does not. Same shape as :one (returns one labeling,
persists nothing).Replace-on-rerun (:all only). A previous :all run's artifacts under Into
are cleared before new ones are written, so re-running after the base moved converges
instead of accreting. A run that grounds no choices clears too. The one exception
is :no-backend — nothing was computed, so the previous artifact is left standing.
The grounding is never stored; :choices is the menu in content order (see build).
Phase timings (:ground-ms = grounding the Program, :translate-ms = rendering ASPIF,
:solve-ms = the solve) ride the result for a profiling caller.
Returns {:base :into :choices [..] :labelings [{:context :true [..] :false [..]}] :count n} (:context nil in :one mode, which persists nothing). :count 0 with
:reason when there is nothing to solve or no ASP backend.
Ground the `assumptionRules` visible from `Base` (honoring their `exceptWhen`
guards), detect the constraints among the ground choice heads — the direct
auto-clashes *and* every `set/hardConstraint` / `set/softConstraint` rule's body
ground into a nogood — and solve.
**`mode` (an optional third argument, default `:all`) picks how many worlds:**
* `:all` — enumerate **every** optimal answer set and materialize each as its own
inert labeling context: a `genlContext` child of `Base` named
`<Into-base><i>Context` (skipping any slot an unrelated context occupies) holding
`(head)` for a chosen-true choice, `(not head)` for a chosen-false one, and its
`labelingOf` ownership marker. The worlds coexist and persist for `do/classify` to
aggregate; base belief is untouched. This is the studying-many-worlds mode, and it
is infeasible where the optima are astronomically many (a large graph coloring has
too many valid colorings to enumerate).
* `:one` — commit to **one** optimal answer set via a single `:label` solve
(minimizing defeated assumptions — keep as much belief as possible), and return it
in the result **without persisting anything**. The solving mode: it wants an
answer, not an artifact, so it is feasible at scale (one solve, no enumeration, no
materialization). `Into` is accepted for a uniform imperative shape but unused.
* `:sat` — `:one`, but plain **satisfaction** rather than optimization: no
keep-belief objective, so clingo stops at the first model instead of proving
cost-optimality over the choice atoms. For a program whose hard constraints
already pin what must be chosen (a graph coloring's hard at-least-one), "keep as
much as possible" is redundant and the optimization is a scaling wall — `:sat`
finishes where `:one` does not. Same shape as `:one` (returns one labeling,
persists nothing).
**Replace-on-rerun (`:all` only).** A previous `:all` run's artifacts under `Into`
are cleared before new ones are written, so re-running after the base moved converges
instead of accreting. A run that grounds *no* choices clears too. The one exception
is `:no-backend` — nothing was computed, so the previous artifact is left standing.
The grounding is never stored; `:choices` is the menu in content order (see `build`).
Phase timings (`:ground-ms` = grounding the Program, `:translate-ms` = rendering ASPIF,
`:solve-ms` = the solve) ride the result for a profiling caller.
Returns `{:base :into :choices [..] :labelings [{:context :true [..] :false [..]}]
:count n}` (`:context` nil in `:one` mode, which persists nothing). `:count 0` with
`:reason` when there is nothing to solve or no ASP backend.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 |