vaelii.impl.asp.edge — com.vaelii/vaelii 0.11.0

The real ASP backend behind vaelii.impl.solve/Solver — the edge solver.

solve.clj describes what an edge solve is: most of the KB is monotonic or default-true with no conflict, so only the contested defeasible nodes are sent, known-true content is fixed background, and contradictions are soft and prioritized so a solve never fails. This namespace renders that Program to ASPIF and reads an answer set back.

The encoding

Each contested assumption is a choice atom: true means believed, false means defeated. Known-true (:fixed) members of a contradiction are not atoms — they hold by assumption, which is exactly what makes them background.

A contradiction #{h1 h2 ...} becomes a violation atom derived from its contested members:

v :- a_h1, a_h2, ...

and a weak constraint minimizing v. Weak rather than hard is the whole point: an unsatisfiable contradiction costs, it does not make the program UNSAT, so it comes back in :violated instead of throwing.

A nogood carrying :hard true (a set/hardConstraint rule ground by solve-context) is instead a hard integrity constraint

:- a_h1, a_h2, ...

with no violation atom and no minimize term: a model satisfying its whole body is excluded outright. That is what makes graph 3-coloring plain satisfaction rather than optimality-proving over soft violations — an adjacency clash is never tradeable. Soft nogoods (the default) keep the minimize path above.

In practice :violated comes back empty, and that is correct rather than a gap. An irreducible known-true clash never reaches a solver: core/settle's decide-nogood classifies it as hard and reports it directly, and solve/program drops any nogood with no contested member. What does arrive always has a contested member, and defeating that member always satisfies it. The :doomed path below is therefore defensive — it costs nothing and stays correct if nogoods ever grow beyond today's S vs (not S) pairs.

The objective, most significant first

Higher ASPIF minimize priorities dominate lower ones, so the levels are:

level	minimizes	why
2 + rank(p)	violation atoms	satisfy contradictions, caller priority first
1	defeated assumptions	give up as little belief as possible
0	a content-keyed weight	break remaining ties stably

Caller priorities are mapped through their ascending rank rather than used as levels directly, so any integers work and none can collide with the two levels below.

Determinism

A tie between equally-good answer sets has no principled winner, but it must not depend on assertion order — the engine-wide invariant in docs/nmtms.md. Atom ids are allocated in solve/content-key order, and level 0 weights defeating the greatest content-key most cheaply, mirroring the stub's choice. Same knowledge in any order, same answer set.

Availability

edge-solver degrades rather than fails when there is no backend at all: with no clingo and no clasp reachable it delegates to solve/local-solver, so installing it is always safe. Degradation is confined to that case on purpose — see below.

A result that is not an answer

A backend's result is an answer set only at :optimum or :sat. :interrupted (the time limit, config/asp-time-limit, or a signal) and :unknown carry no witness, and every reader here maps an atom's absence to defeated or not kept — so read as an answer, an empty result defeats every contested assumption and labels every choice head false. answered? gates each reader.

With a backend present, edge-solver decides nothing rather than degrading. The stub and ASP disagree — measured on two nogoods sharing a member, the stub defeats {1,3} where the optimum defeats {2} — and the two are not interchangeable halves of one answer. A labeling solve that runs out of budget while the classification solve beside it finishes would pair a stub labeling with an ASP classification, which label/check-agrees reports as :labeling-inconsistent, blaming the encoding for a disagreement the fallback introduced. Worse across a settle's defeat rounds: round 1 interrupted and round 2 not yields a belief set neither solver would produce, differing run to run on identical knowledge — the order-independence invariant in docs/nmtms.md is a claim about knowledge, and a wall clock is not knowledge. So undecided is returned instead: no defeat, the contested assumptions all stand, and :error names what went wrong for a caller that can act on it. With no backend the two degrade together and stay consistent for free — classify-program claims nothing without one — which is why that case, and only that case, still falls back.

A backend that throws — clingo's :solver-failed, clasp's :solver-unavailable, a JNA Error against a missing libclingo — reads the same way, and the catch is here rather than at the caller because this is the seam a native failure crosses. Left to propagate it would unwind whatever arbitration was in progress: settle's resolve-contradictions calls the solver after an earlier round already mutated the TMS, so the throw would leave a half-arbitrated KB behind — stale :conflicts, settle-finish never reached, reset-touched! never run. undecided leaves the KB as the round found it and hands the failure back as data.

:unsat is different and keeps its own reading: a definite no model, the same answer in every run, so it costs the invariant nothing. Each reader has a word for it — edge-solver degrades, kept-of keeps nothing, enumerate-optima is empty.

The imperative readers (kept-of, enumerate-optima, classify-program) refuse an unanswered result with :solver-failed rather than return a world nobody computed. They are not mid-arbitration, so a throw there costs nothing and says more.

classify-program clj

(classify-program {:keys [assumptions fixed] :as program})

Classify program's assumptions into :true / :supportable / :false by brave/cautious reasoning over its optimal answer sets — in every optimum, in some, in none.

:fixed handles are reported :true: known-true background is assumed by every model, which is what makes it background rather than something the solver decides. With no ASP backend every contested assumption is genuinely one of several options, so it is reported :supportable and nothing is claimed forced or excluded. An enumeration the backend did not finish is refused (:solver-failed): a cautious set read off a cut-short stream would call forced what was merely not yet ruled out.

Below vaelii.core on purpose — the classification is a property of the encoding and the backend, not of any KB — so settle can stamp it onto the TMS as belief settles. asp.label re-exports it for the KB-level callers that predate the move.

edge-solver clj

An ASP-backed solve/Solver. Install with (core/set-solver kb edge-solver).

Falls back to solve/local-solver when no ASP backend is reachable, so this is safe to install unconditionally; check (solver/available?) if you need to know which one will run. With a backend present it answers from the backend or decides nothing — it never mixes the two, and it never throws (see the ns docstring, and undecided).

enumerate-optima clj

(enumerate-optima {:keys [assumptions] :as program})

Every optimal answer set of program, each as the set of its chosen-true assumption handles — the raw material for materializing one labeling context per answer set (docs/solving.md).

Uses the solver's :all-optima mode over the tiebreak-off encoding, so genuinely tied optima come back as distinct witnesses rather than collapsing to one. A witness's atom labels are mapped back through handles-of.

Returns:

• [] — no assumptions (nothing to decide; the caller makes no labeling);
• nil — no ASP backend (enumeration needs one; the caller reports that);
• [#{h} …] — one handle-set per optimum otherwise.

With assumptions but no nogoods every choice can be kept, so the single optimum keeps them all; a functional/disjoint/¬ clash is what splits the optima apart. A program whose hard constraints admit no model is :unsat and enumerates to []; an enumeration the backend did not finish is refused (:solver-failed) rather than returned as the optima it happened to reach.

kept-of clj

(kept-of {:keys [table assumptions]} result)

The chosen-true assumption handles of one :label answer set, read back through translation t's atom table — the single-answer-set counterpart to interpret's defeat set (kept = assumptions − defeated). solve-context's :one mode reads a labeling with it. An :unsat result carries no true labels, so this returns #{} (nothing kept); an :interrupted or :unknown one is refused (:solver-failed), since its empty atom list would read the same way and mean nothing.

translate clj

(translate program)

(translate {:keys [assumptions contradictions] :as program}
           {:keys [tiebreak? keep-belief?]
            :or {tiebreak? true keep-belief? true}})

Render program to ASPIF. Returns

{:aspif      text or nil          ; nil when there is nothing to solve
 :table      the atom table
 :by-label   {label nogood}       ; violation atom -> the contradiction
 :assumptions [handle ...]        ; in content-key order
 :doomed     [nogood ...]}        ; all-fixed, unsatisfiable without solving

:tiebreak? (default true) emits the level-0 content-keyed objective that makes the optimum unique. Solving for one labeling wants it — an arbitrary choice still has to be a stable one. Enumerating optima wants it off: it is an arbitrary preference, not a semantic constraint, and leaving it in collapses every tie to a single answer set, which would report a genuinely open choice as forced. label/classify-program is the caller that turns it off.

:keep-belief? (default true) emits the level-1 objective that minimizes defeated assumptions — keep as much belief as possible. Turning it off makes the solve plain satisfaction rather than optimization: with no minimize term clingo stops at the first model instead of proving cost-optimality over the choice atoms, which is the difference between finishing and not at scale (a 10k-node graph 3-coloring). A caller turns it off only when the program's hard constraints already pin what must be chosen (e.g. a hard at-least-one), so "keep as much as possible" adds nothing.