Counterfactual instances on UNSAT (proposal + implementation)#337
Open
sidprasad wants to merge 3 commits into
Open
Counterfactual instances on UNSAT (proposal + implementation)#337sidprasad wants to merge 3 commits into
sidprasad wants to merge 3 commits into
Conversation
Adds Notes/counterfactual-unsat.md sketching a relaxation pass in
the Forge/Pardinus layer: on UNSAT, drop minimum core formulas,
re-solve, and return a near-instance plus the dropped constraint
list over the existing Sterling websocket.
Scope is intentionally narrow to the Racket-side work:
- new RelaxedSat result type
- naive drop-and-retry relaxation loop in
forge/solver-specific/pardinus.rkt
- new status "counterfactual" + dropped field on the JSON
envelope (extending the channel PR #312 already established)
- real instance XML via the existing SAT path in modelToXML.rkt
Sterling / CopeAndDrag-side rendering (custom themes, per-tuple
violation annotations) is explicitly out of scope and treated as
a downstream follow-on PR against the CnD repo.
Builds on PR #312 (Nelson, Nov 2025), which already plumbed the
unsat core onto the Sterling websocket. No code yet.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Implements the solver-side relaxation pass described in
Notes/counterfactual-unsat.md. When a Forge run returns UNSAT and the
new `counterfactual` option is `on`, the Pardinus backend now drops one
core formula at a time, re-solves under a fresh run-name, and on success
returns a RelaxedSat carrying both the satisfying instance and the list
of dropped formulas.
Files touched:
* forge/sigs-structs.rkt
- RelaxedSat substruct of Sat (so all existing consumers — modelToXML,
lazy tree, is-sat? — treat it as a normal SAT instance and render
through the existing SAT path).
- New options: `counterfactual` ('on/'off, default 'off) and
`counterfactual_budget` (non-negative integer, default 5).
* forge/solver-specific/pardinus.rkt
- send-to-kodkod refactored: the problem-emission logic moved into a
local `emit-problem` helper that takes a dropped-ID set; the initial
problem is emitted with no drops.
- A `relax-context` closure (built only when the option is on) re-uses
`emit-problem` to re-issue the whole problem under fresh run-names
with the chosen assertions replaced by `true`. Returns 3 values now:
(all-rels core-map relax-context).
- get-next-kodkod-model takes relax-context as an extra argument and,
on a fresh UNSAT with core, runs `run-relaxation-loop` — naive
drop-and-retry, smallest top-level assertion first, deterministic.
The loop bails out after `counterfactual_budget` iterations or when
the core only references already-dropped assertions.
- Once we've entered relaxation, subsequent "next instance" requests
are routed to the relaxed run-name (kept in a box inside
relax-context), so clicking "next" on a counterfactual doesn't
silently drop the user back to UNSAT.
* forge/send-to-solver.rkt
- Typed contract widened: send-to-kodkod returns (Values Any Any Any);
get-next-kodkod-model takes an extra Any. cvc5 backend unchanged.
* forge/server/forgeserver.rkt
- make-status-value: RelaxedSat? checked before Sat? so relaxed
results report status "counterfactual" rather than "sat".
- New `make-dropped-value` helper deparses the dropped-formulas list
using the same machinery as `make-core-value` (shared
`deparse-formula-entry`).
- JSON envelope gains a `dropped` field alongside `core`. Older
Sterling clients ignore unknown fields and fall back to the SAT
rendering path (since `status` is unknown to them and the XML body
*is* a real instance), which is the correct degradation.
modelToXML.rkt needed no changes: because RelaxedSat is a Sat substruct,
the existing cond chain in solution-to-XML-string already routes it
through the SAT-instance generator.
Smoke-tested four cases against MiniSatProver:
- single-drop counterfactual (drops `no edges`, returns SAT instance)
- multi-drop counterfactual (drops two assertions over two iterations)
- normal SAT with counterfactual on (no relaxation triggered)
- normal UNSAT with counterfactual off (regression: unchanged path)
CnD / Sterling-side rendering of the new status and dropped field is
out of scope for this commit and tracked as a follow-on against the
CopeAndDrag repo.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For each formula dropped during counterfactual relaxation, walk its AST
to collect the sigs and fields it references, then annotate every tuple
of those relations in the relaxed instance with `violates_cN`="true"
(where N indexes the dropped formula). The annotations ride on the
existing tuple-annotations channel in modelToXML, so they surface in
the per-tuple XML attributes the visualizer already consumes.
This is the Amalgam-flavored half of the proposal — coarse, not full
per-tuple provenance. We say "look here: these relations are involved
in the dropped constraint," not "this specific tuple is the
unsatisfying witness." Full witness extraction would need an evaluator
pass per dropped formula (probably another commit cycle); this gives
the visualizer enough signal to direct user attention without that
plumbing.
New module forge/server/counterfactual-witness.rkt provides:
- collect-referenced-relations: AST walker pulling every
node/expr/relation reachable from a formula or expression. Handles
every node type Forge currently constructs (op-on-exprs,
comprehensions, quantified formulas, multiplicity, ite, pred/fun
spacers, int expressions, ...). Opaque entries (string fallbacks
from Pardinus, sealed formulas) contribute no relations.
- build-witness-tuple-annotations: turns (dropped-formulas, instance)
into the nested hash shape modelToXML's tuple-annotations expects.
Tuples in multiple dropped formulas' relations accumulate multiple
violates_cN annotations.
forge/server/forgeserver.rkt: both get-xml definitions (display-model
and start-sterling-menu) now populate tuple-annotations from RelaxedSat
results before handing them to solution-to-XML-string. Non-RelaxedSat
results get the empty hash, same as before.
Unit-tested with a direct test (a hand-built `no edges` formula against
a fake instance) — walker finds `edges`, both edges tuples get
violates_c0=true. End-to-end smoke tests still pass.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds counterfactual UNSAT relaxation to Forge: when a
runis UNSAT and the user opts in withoption counterfactual on, the Pardinus backend drops one core formula at a time, re-solves, and returns a near-instance plus the list of dropped constraints. The visualizer renders the near-instance through the existing SAT path; tuples of relations referenced by dropped formulas getviolates_cNXML annotations.Three commits, in this order:
5e61c548— Design doc (Notes/counterfactual-unsat.md). Scope is narrowed to Forge/Pardinus + minimum wire format; CnD-side rendering is explicitly out of scope for this PR. Builds on PR Modify the cores pipeline to get cores info to Sterling #312 (Nelson, Nov 2025) which already put the unsat core on the Sterling websocket.5db29013— Core implementation. NewRelaxedSatsubstruct ofSat; newcounterfactual(on/off) andcounterfactual_budget(int) options; relaxation loop inpardinus.rkt; new"counterfactual"status +droppedfield on the Sterling JSON envelope.915db5f2— Relation-level witness flagging. Newforge/server/counterfactual-witness.rktwalks each dropped formula's AST and tags every tuple of any referenced relation withviolates_cN="true"via the existingtuple-annotationschannel inmodelToXML.How it works
send-to-kodkodbuilds arelax-contextclosure (only when the option is on) that captures everything needed to re-emit the problem under a fresh run-name with selected assertion IDs replaced bytrue. On UNSAT with core,get-next-kodkod-modelentersrun-relaxation-loop— naive drop-and-retry, smallest top-level assertion first (deterministic), bailing out atcounterfactual_budgetiterations or when the core only mentions already-dropped assertions.RelaxedSatinherits fromSat, soSat?returns true for it —modelToXML.rktneeded zero changes (the SAT branch already handles the instance). Only the wire-format code (forgeserver.rkt) needs to dispatch onRelaxedSat?first.Test plan
no edges && some edges→ dropsno edges, returns SAT instanceno edgesformula → walker findsedges→ both tuples flagged)forge/tests/) to confirm no regressions on unrelated pathsstatus: "counterfactual"+droppedfield +violates_cNtuple attributes (separate PR against the CopeAndDrag repo)Out of scope (per design doc)
statusanddroppedand fall back to SAT rendering — graceful degradation.🤖 Generated with Claude Code