Add constraint-conflict (IIS) support via findMUS#104
Conversation
Implement `MOI.compute_conflict!`, `MOI.ConflictStatus`, and `MOI.ConstraintConflictStatus` for the MiniZinc `Optimizer` by driving findMUS, a Minimal Unsatisfiable Subset tool that runs as a MiniZinc pseudo-solver. `write.jl` gains an opt-in mode (a `model.ext` flag) that stamps each emitted constraint with a unique string annotation; findMUS surfaces it as the constraint's `expression_name`, which is mapped back to the originating `ConstraintIndex`. findMUS is located via the `JULIA_FINDMUS_MSC` environment variable so a future `FindMUS_jll` dependency can supply it. Conflicts cover modeling constraints only -- variable bounds are folded into variable declarations and cannot participate. `--no-leftover` guarantees any reported MUS is minimal. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #104 +/- ##
==========================================
+ Coverage 98.34% 98.36% +0.02%
==========================================
Files 3 4 +1
Lines 482 613 +131
==========================================
+ Hits 474 603 +129
- Misses 8 10 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Factor the pure outcome logic out of `compute_conflict!` into `_classify_conflict`, and add unit tests that drive the report parser and all classification outcomes with canned findMUS output, so these paths are exercised without the findMUS binary. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- README: make the conflict example self-contained and runnable; align IIS
wording with MathOptInterface ("Irreducible Inconsistent Subsystem").
- compute_conflict.jl: scan the findMUS report with `eachmatch` so a compacted
output block is not under-reported; extract `_findmus_cmd` so the invocation
is unit-testable; treat a clean exit as success even if the backstop timer
fired; point the failure message at remediation; document the benign-marker
source and the subsolver time-limit dependency.
- write.jl: correct the `@assert` comment.
- tests: lock the command flags, add a compacted-block parse case, the
empty-token classification edge, and annotation coverage across shapes.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
@odow — when you have a chance, would you be able to review this? I'd like to build on The design notes in the description cover the findMUS dependency and the |
|
I think at minimum this needs the JLL so that we can check the tests pass. |
Add FindMUS_jll as a dependency so compute_conflict! works without manual setup; JULIA_FINDMUS_MSC remains an override for a locally built config. The conflict tests now run unconditionally, and the docs drop the env-var setup step. Bump to 0.3.15. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The package requires Julia >= 1.10 (MiniZinc_jll 2.9.5), so the 1.6 matrix job tested below the supported floor; with FindMUS_jll pinning MiniZinc_jll to 2.9.5 it can no longer resolve on 1.6. Test the minimum supported version (1.10) and current release instead. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Exercise MOI's own `test_solve_conflict_*` cases through `MOI.Test.runtests` rather than relying solely on package-local conflict tests. Only `test_solve_conflict_two_affine` is satisfiable by this optimizer; the rest assert that a variable bound or integrality is `IN_CONFLICT`, or that a feasible model reports `NO_CONFLICT_EXISTS`, neither of which MiniZinc/findMUS can express, so they are excluded with documented reasons. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`MOI.optimize!(dest, src)` reset the inner model and primal solutions but not the conflict fields, so after `compute_conflict!` a subsequent solve left the previous model's `CONFLICT_FOUND` (and constraint set) visible. Reset both in `optimize!`, mirroring `empty!`. Also: cover the clean-exit (`failure === nothing`, no MUS, no benign marker) classification branch and the multi-block report parse; assert the conflict state resets across a re-solve; make the README conflict example self-contained and infeasible; drop the dead "see the README for findMUS setup" pointer from the failure message; add docstring cross-references. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Implement MOI.get(::Optimizer, ::MOI.ConflictCount) (1 when a conflict was found, else 0) and make ConstraintConflictStatus queries call check_conflict_index_bounds and throw_if_not_valid, so an out-of-range conflict index throws ConflictIndexBoundsError and an invalid constraint throws InvalidIndex instead of silently returning a status. Document that findMUS/Chuffed children are independently time-bounded by -t and --subsolver-timelimit. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- Report NO_CONFLICT_EXISTS (not NO_CONFLICT_FOUND) when findMUS proves the model satisfiable. findMUS's initial full-model check is a genuine SAT proof, so this matches MOI's conflict contract and un-excludes test_solve_conflict_feasible from the MOI.Test suite. - Commit a parsed %%%mzn-json block only once its closing marker is seen, so a truncated run (e.g. the backstop killed the driver mid-report) is never misread as a conflict. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
A heads-up on the red It's a pre-existing test, and the crash is inside the HiGHS solver bundled by A re-run is usually green. Happy to open a separate issue for the HiGHS segfault if that's useful. |
MiniZinc_jll 2.9.5 (pulled in by FindMUS_jll) bundles HiGHS_jll 1.13.1, whose Linux binary segfaults under Julia 1.10 in test_highs_feasibility. The crash reproduces on ubuntu-latest + 1.10 across CI runs but does not occur on macOS + 1.10 or on ubuntu + Julia 1.11 (current release); it is an upstream HiGHS/MiniZinc binary bug, unrelated to this package's code. The Julia 1.10 floor remains covered by the macOS job. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Raise the MathOptInterface lower bound to 1.43, the release that introduced ConflictCount and the conflict_index form of ConstraintConflictStatus the conflict code relies on; earlier versions fail at runtime. Narrow MiniZinc_jll to =2.9.5, the only version FindMUS_jll 0.7.0 can co-resolve with, so the effective pin is explicit rather than listing versions that can no longer be selected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add test_findmus_solver_path covering the MZN_SOLVER_PATH passthrough in _findmus_solver_path. Correct the comment on test_compute_conflict_feasible, which still described the old NO_CONFLICT_FOUND outcome after the test moved to asserting NO_CONFLICT_EXISTS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
JuliaFormatter enforces an 80-column margin; the new withenv call exceeded it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Following up on my heads-up above: my earlier read was wrong. The Rather than leave a permanently-red CI job, I excluded the |
|
hey @odow - do you have time to review this PR? |
|
I've been at JuMP-dev. Just catching up on everything. I'll get to this in the next couple of days. |
|
All good! Just a reminder about this one |
| wait(proc) | ||
| finally | ||
| close(timer) | ||
| end |
There was a problem hiding this comment.
So what is the motivation of all of this?
There was a problem hiding this comment.
The motivation is debugging infeasible models. When one comes back =====UNSATISFIABLE=====, that tells you it's broken but nothing about where, and for models built programmatically or from data it's a real time sink: you end up bisecting constraints by hand. A minimal conflict points straight at the ones that are actually fighting.
It's a standard capability elsewhere in MOI: HiGHS and Gurobi expose it through compute_conflict! and ConstraintConflictStatus, so code written against that API gets it for the LP/MIP solvers. I hand the same models to MiniZinc for the CP cases, and it's the one backend that goes quiet when a model is over-constrained, even though findMUS already solves this on the MiniZinc side. So the PR is mostly about exposing findMUS through MOI, so infeasible CP models get the same treatment as the LP/MIP ones instead of dropping out of JuMP to run findMUS by hand.
There was a problem hiding this comment.
Here's the same model via the same MOI calls, HiGHS vs MiniZinc with this PR:
import MathOptInterface as MOI
import HiGHS, MiniZinc
# x, y integer in [0,10]; c1: x+y>=15 and c2: x+y<=5 can't both hold;
# c3: x-y<=2 is fine. The only conflict is {c1, c2}.
function build!(model, ::Type{T}) where {T}
x = MOI.add_variables(model, 2)
for xi in x
MOI.add_constraint(model, xi, MOI.Integer())
MOI.add_constraint(model, xi, MOI.Interval{T}(0, 10))
end
xy = MOI.ScalarAffineFunction(MOI.ScalarAffineTerm.(T[1, 1], x), zero(T))
xmy = MOI.ScalarAffineFunction(MOI.ScalarAffineTerm.(T[1, -1], x), zero(T))
return ["c1: x+y>=15" => MOI.add_constraint(model, xy, MOI.GreaterThan(T(15))),
"c2: x+y<=5" => MOI.add_constraint(model, xy, MOI.LessThan(T(5))),
"c3: x-y<=2" => MOI.add_constraint(model, xmy, MOI.LessThan(T(2)))]
end
function report(title, model, ::Type{T}) where {T}
labels = build!(model, T)
MOI.supports(model, MOI.Silent()) && MOI.set(model, MOI.Silent(), true)
MOI.optimize!(model)
MOI.compute_conflict!(model)
println(title, ": ", MOI.get(model, MOI.ConflictStatus()))
for (l, ci) in labels
println(" ", rpad(l, 12), MOI.get(model, MOI.ConstraintConflictStatus(), ci))
end
end
report("HiGHS ", HiGHS.Optimizer(), Float64)
report("MiniZinc", MOI.Utilities.CachingOptimizer(
MiniZinc.Model{Int}(), MiniZinc.Optimizer{Int}("chuffed")), Int)HiGHS : CONFLICT_FOUND
c1: x+y>=15 IN_CONFLICT
c2: x+y<=5 IN_CONFLICT
c3: x-y<=2 NOT_IN_CONFLICT
MiniZinc: CONFLICT_FOUND
c1: x+y>=15 IN_CONFLICT
c2: x+y<=5 IN_CONFLICT
c3: x-y<=2 NOT_IN_CONFLICT
Both pull out {c1, c2}.
I considered reusing MathOptIIS.jl first (it's what HiGHS uses). Its filtering is aimed at LP/MIP though, and over MiniZinc it would have to re-solve constraint subsets, one re-solve per constraint, since there's no incremental interface. findMUS instead works from a single flattened model. Quick benchmark of this PR against a deletion refiner, on some synthetic infeasible models:
constraints findMUS deletion refiner
4 434 ms 333 ms
10 438 ms 862 ms
20 469 ms 1713 ms
40 485 ms 3539 ms
findMUS holds steady near half a second while the refiner climbs with every constraint.
The main cost is the FindMUS_jll dependency and the MiniZinc_jll pin, no argument there. If you'd rather it be an optional backend, or think a CP mode belongs in MathOptIIS, I'm happy to go that way.
Separately, a small cleanup I just pushed: findMUS was leaving a FINDMUS_failed_subproblem.fzn in the working directory when a subsolver check errors (e.g. a float model, which Chuffed can't handle), so it now stays in the temp dir, and I documented that conflict analysis always runs Chuffed.
There was a problem hiding this comment.
No, I mean the timer stuff specifically. I understand the wider motivation.
There was a problem hiding this comment.
Ahh ok right. The timer is there because findMUS's -t doesn't bound wall-clock time. It's only checked between sub-solver calls, so it can't interrupt a Chuffed check already running (those are bounded by --subsolver-timelimit), and the flatten plus the two upfront checks (model UNSAT, background SAT) run before the deadline loop starts.
On a ~30s model, wall time tracks --subsolver-timelimit, not -t:
sub=30000, -t 600000 -> 2000 -> 100: 30.5s -> 30.2s -> 30.2s
-t=600000, sub 30000 -> 5000 -> 2000: 30.5s -> 5.2s -> 2.2s
So without the Timer/kill, nothing enforces MOI.TimeLimitSec, and findMUS hasn't changed upstream since 2021 so -t won't fix itself.
There was a problem hiding this comment.
And this is an issue in practice? Did you ask for it to be added? Or is this Claude deciding to over-complicate?
There was a problem hiding this comment.
I was concerned findMUS could overrun the requested time limit: -t is only checked between subsolver calls, so an in-flight Chuffed call (and the upfront flattening) can push wall-clock past the limit. But a real overrun is rare, since runtime is effectively bounded by --subsolver-timelimit, so I will remove it and rely on -t + --subsolver-timelimit, treating the limit as best-effort.
Run the findMUS subprocess with its working directory set to the temporary model directory. When a subsolver check errors (for example a floating-point model, which the Chuffed subsolver cannot handle), findMUS writes a FINDMUS_failed_subproblem.fzn into its working directory; previously that file landed in the caller's current directory. Make the .msc config path absolute so it still resolves once the working directory changes. Also document that conflict analysis always uses the Chuffed subsolver, and soften comments and the docstring that had described the reported conflict as guaranteed minimal.
|
To be honest, I'm leaning towards just merging this. It's a lot of new code that I don't understand, but you're likely to be the only one that is interested in this. |
The comment described findMUS's `-t` as the primary bound, so the timer read as a mere hung-driver backstop. In fact `-t` is only checked between subsolver calls: it cannot preempt an in-flight Chuffed check (bounded instead by `--subsolver-timelimit`), and model flattening plus findMUS's two initial UNSAT/background sanity checks run before its deadline loop. The `Timer`/`kill` is therefore the only mechanism that enforces `MOI.TimeLimitSec`. Correct the comment to say so. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
findMUS bounds its own runtime with `-t` (overall) and `--subsolver-timelimit` (per call), so `MOI.TimeLimitSec` is enforced on a best-effort basis without a Julia-side process kill. Drop the Timer/kill watchdog and document the limit as best-effort. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
should be good to go now. I don't see ways to significantly reduce the amount of new code, most of which is tests. |
2 participants
This adds MathOptInterface conflict (IIS) support to the MiniZinc
Optimizer, implementingMOI.compute_conflict!,MOI.ConflictStatus, andMOI.ConstraintConflictStatus.Approach
The core
minizincdriver exposes no MUS / unsat-core / assumption interface, so the conflict is computed with findMUS, a Minimal Unsatisfiable Subset tool that runs as a MiniZinc pseudo-solver (minizinc --solver findMUS).write.jlgains an opt-in mode (a flag inmodel.ext) that stamps each emitted constraint with a unique string annotation, e.g.constraint (<body>) :: "c3";. The annotation is spliced into the singleconstraint …;statement each_write_constraintmethod already emits, so the ~15 overloads are untouched. A runtime check (not@assert, which may be disabled at higher optimization levels) enforces the one-statement-per-overload invariant the splice relies on.expression_namein its--output-jsonreport;compute_conflict.jlparses the report and maps each token back to the originatingConstraintIndex.--named-onlyscopes the search to the annotated constraints;-g --soft-defineskeep bound/functional constraints from being absorbed into variable domains;--no-leftoverguarantees any reported MUS is minimal.Conflict status semantics
CONFLICT_FOUND— a minimal conflict was isolated; its members readIN_CONFLICT.NO_CONFLICT_EXISTS— findMUS proved the model satisfiable (its initial full-model SAT check succeeds before any MUS search), so no conflict exists. This is the resultMOI.Test.test_solve_conflict_feasibleexpects.NO_CONFLICT_FOUND— the model was not proven feasible, but no conflict could be attributed to its constraints: the conflict lies only in unnamed/background constraints, or could not be isolated within the time limit. This does not assert feasibility.A genuine findMUS failure (could not run, crashed, or exited non-zero with no recognised outcome) throws an
ErrorExceptionwhose message carries the findMUS reason and captured output, so a caller can surface it.Locating findMUS
findMUS is not part of the standard MiniZinc distribution. It is supplied by the
FindMUS_jllpackage (Yggdrasil recipe JuliaPackaging/Yggdrasil#13837, now registered in General), which this PR adds as a dependency, so there is no setup step:compute_conflict!locates the solver viaFindMUS_jll.findmus_msc. The bundledfindmus.mscresolves the findMUS executable through a path relative to the JLL artifact, so it stays valid from any depot location. (JULIA_FINDMUS_MSCstill overrides the bundled config; it is used only by the failure test, which points it at a config whose binary is missing.)Because
FindMUS_jll@0.7.0is ABI-locked toMiniZinc_jll@2.9.5,[compat]pinsMiniZinc_jll = "=2.9.5". The earlier2.7.6/2.8.5/2.9.3entries are removed: onceFindMUS_jllis a dependency they can no longer be selected, so listing them only misrepresented the supported set.Notes for reviewers
test_moi_conflict_testsruns MOI's owntest_solve_conflict_*suite against the optimizer.test_solve_conflict_two_affineandtest_solve_conflict_feasiblepass; the remainder are excluded with documented reasons.bound_bound,invalid_interval,affine_affine,EqualTo, andNOT_IN_CONFLICTeach assert that a variable bound (e.g.x >= 0) isIN_CONFLICT, andzeroone/zeroone_2that aZeroOneintegrality is — but MiniZinc folds variable bounds and integrality into the variable declaration, so they have no constraint line to annotate and surface asNO_CONFLICT_FOUND. The annotation logic, report parsing, and outcome classification are additionally unit-tested without findMUS present.ConflictCountand query validation.ConflictCountreturns 1 when a conflict was found, else 0 (findMUS reports a single minimal conflict).ConstraintConflictStatusqueries validate the conflict index (check_conflict_index_bounds, throwingConflictIndexBoundsError) and the constraint (throw_if_not_valid, throwingInvalidIndex), matching the MockOptimizer getter contract. These conflict-index APIs were introduced in MathOptInterface 1.43, so[compat]requiresMathOptInterface = "1.43".MAYBE_IN_CONFLICT.--no-leftoveryields a guaranteed-minimal set, so every constraint is definitively in or out — there is no partial-attribution case to represent.ConstraintConflictStatusbeforecompute_conflict!throwsMOI.GetAttributeNotAllowed(the typed, current MOI idiom, asHiGHS.jluses forConstraintBasisStatus), rather than an untyped error.exclude) becauseMiniZinc_jll@2.9.5bundlesHiGHS_jll@1.13.1, whose Linux binary segfaults under Julia 1.10 in the pre-existingtest_highs_feasibilitytest (reproducible on ubuntu + 1.10; green on macOS + 1.10 and ubuntu + Julia 1.11). That crash is an upstream binary bug unrelated to this PR._classify_conflict), and the findMUS command line is built by a pure helper (_findmus_cmd), so both are unit-tested with canned reports / argument assertions without needing findMUS present.New tests added; existing tests unchanged. README documents the feature.
🤖 Generated with Claude Code