Skip to content

Minimal Unsatisfiable Core Extraction

Method — instantiates Incompatible Requirement Set Resolution

Given a set already proven to have no joint solution, strips it down to a smallest subset that is still unsatisfiable — the irreducible knot of commitments that actually clash.

Knowing a requirement set is infeasible tells you nothing about where the fault lies — the offending clash may live among any few of hundreds of commitments. Minimal Unsatisfiable Core Extraction localizes it: starting from a set proven unsatisfiable, it removes members until it reaches an irreducible core — a subset that is still unsatisfiable but becomes satisfiable the instant any one member is dropped. Its defining move is localization by irreducibility: it converts a global "somewhere in here, these can't all hold" into a precise "*these three, and only these three, are the conflict," which is exactly what turns an unbounded hunt into a bounded negotiation. It is the natural answer to the archetype's nastiest case — a conflict that is real jointly even though every pair is compatible — because the core it returns can be a trio (or larger) in which no two members clash on their own.

Example

A product configurator encodes a few hundred option rules for a build-to-order laptop. Marketing adds "Chassis = Ultralight implies Battery = Standard"; thermal engineering adds "Battery = Standard implies not Discrete-GPU"; sales adds "the Creator bundle includes both Chassis = Ultralight and Discrete-GPU." Each rule is defensible, and every pair of them is jointly satisfiable — but the three together admit no valid Creator-bundle laptop, so the configurator reports "no configuration" with no hint why. Core extraction runs the satisfiability check repeatedly: it tentatively drops each rule and re-tests, keeping only rules whose removal restores satisfiability. It converges on exactly those three, clearing the other several hundred, and emits a short conflict record naming the implication chain. The fix is now a scoped, three-way conversation between marketing, thermal, and sales — not an audit of the whole rule base. A deletion-based loop like this, or the divide-and-conquer QuickXplain strategy, is the standard way to pull such a core.

How it works

The method wraps a satisfiability oracle in a shrinking loop. In the simplest deletion-based form, walk the constraints one at a time: provisionally remove a constraint and re-test the remainder; if it is still unsatisfiable, that constraint was inessential and stays out; if removal makes it satisfiable, the constraint is part of the core and goes back. QuickXplain does the same job with a recursive split to cut the number of oracle calls. What distinguishes the method from the check it calls is that it produces no satisfiability verdict of its own — it consumes them — and adds one thing: minimality. The output is the small, self-contained set of genuinely conflicting commitments plus an explanation of how they collide.

Tuning parameters

  • Minimal vs. minimum — minimal means no proper subset is unsatisfiable (irreducible, cheap to reach); minimum means the globally smallest such set (far more expensive to certify). Most decisions need only a minimal core.
  • Which core — cores are not unique; a preference order (drop newest constraints first, or lowest-priority first) steers extraction toward the core you can most readily act on.
  • Constraint granularity — extract over individual clauses or over grouped "assumption" constraints (group-MUS), so the core points at meaningful requirements rather than internal encoding artifacts.
  • Oracle-call budget — deletion-based is simple but makes many calls; QuickXplain trades logic for fewer; cap the budget on large sets.
  • Explanation verbosity — from the bare core to an annotated record tracing the implication chain that makes the members inconsistent.

When it helps, and when it misleads

Its strength is that it converts a demoralizing global "infeasible" into a small, precise, ownable conflict — it ends the waste of optimizing inside an empty region, and the extracted core doubles as a compact certificate anyone can independently re-check.

Its central trap is that cores are not unique: the one you extract is a minimal conflict, not the cause, and resolving it does not guarantee satisfiability — a second, independent core may remain, so a set can stay infeasible after the "fix."[1] A core pulled over raw encoding clauses can also point at translation artifacts rather than real requirements if the grouping is wrong. The classic misuse is presenting the extracted core as if it named the single guilty party, when which member should yield is still an open governance question. The discipline that keeps it honest is to re-run the satisfiability check after resolving a core (repeat until satisfiable), extract over meaningful requirement groups, and label the result "a minimal conflict," never "the reason."

How it implements the components

Minimal Unsatisfiable Core Extraction fills the localization side of the archetype — the components that pin down and certify where the incompatibility lives:

  • minimal_unsatisfiable_core — its namesake output: the irreducible offending subset, with the guarantee that dropping any member restores satisfiability.
  • incompatibility_certificate — the core is a self-contained, re-checkable certificate of infeasibility for the whole set (still unsatisfiable on its own; satisfiable if reduced).
  • conflict_explanation_record — the annotated "these members, via this implication chain, admit no joint solution" account that makes the clash legible to the people who own the commitments.

It does not decide satisfiability of the full set (joint_satisfiability_model, feasible_set — that's SAT/SMT Satisfiability Check, which it calls repeatedly) or choose which core member should yield (relaxation_option, constraint_priority_rule, exception_authority — that's Weighted MaxSAT or Soft-Constraint Optimization and Stakeholder Frontier Review).

  • Instantiates: Incompatible Requirement Set Resolution — supplies the localized, certified conflict that the relaxation and governance steps then act on.
  • Consumes: SAT/SMT Satisfiability Check — the shrinking loop is driven by repeated satisfiability queries against a solver.
  • Sibling mechanisms: SAT/SMT Satisfiability Check · Weighted MaxSAT or Soft-Constraint Optimization · Impossibility-Theorem Instantiation Review · Stakeholder Frontier Review · Proof Checking · Constraint-Satisfaction Solver Pass · Compatibility Matrix · Requirements Traceability Matrix · Constraint Relaxation Experiment · Pareto Frontier Analysis · Scenario Sensitivity Sweep · Scope-Boundary Stress Test · Decision Record with Residue

Notes

Resolving one core does not prove the rest satisfiable — there can be several disjoint conflicts. Always re-run the satisfiability check after a fix and keep extracting until the set finally comes back satisfiable (or the surviving core is one you decide to relax through the governance path).

References

[1] A minimal unsatisfiable subset need not be unique — an infeasible set can contain several distinct minimal cores — and finding a minimum (smallest overall) one is harder than finding a merely minimal (irreducible) one. This is why resolving a single core is not a guarantee of feasibility and why the "which core" choice matters. ↩