vaelii.impl.asp.edge — com.vaelii/vaelii 0.1.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: with no clingo and no clasp reachable it delegates to solve/local-solver, so installing it is always safe.

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.

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.

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.

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).

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.