Conflict Diagnosis (Unsat Core)

Problem Class	Solver	Key APIs	Links
Infeasibility Diagnosis / Unsat Core	Z3 (@ohtaman/washi/solvers/z3)	m.integer(), m.continuous(), implies(), m.constraint(), expr, m.check(), m.conflicts	Open in Playground Source Code

When business rules, budgets, and operational policies grow complex, constraints can easily conflict. Because a standard optimization call (m.solve()) only reports "Infeasible", WaSHI provides m.check() to pinpoint conflicting rules without manual trial-and-error.

This example shows how to isolate the conflicting constraint subset using Z3 Unsat Core extraction.

The Conflicting Scenario

A tech team is staffing a customer project:

1. Each engineer costs $8,000 against the project budget (budget_limit).
2. The customer requires rush delivery (rush_required).
3. Rush delivery mandates at least 8 engineers (rush_staffing_rule).
4. The board has imposed a strict budget cap of $50,000 (strict_board_budget_cap).
5. Labor law requires at least 1 employee on staff (minimum_one_employee).

Notice that:

$$8 \text{ engineers} \times \$8,000 = \$64,000 > \$50,000 \text{ budget!}$$

Implementation in WaSHI

import { Model, implies, expr } from "@ohtaman/washi";
import "@ohtaman/washi/solvers/z3";

async function diagnoseConflicts() {
  const m = new Model({ name: "ConflictDiagnosis", solver: "z3" });

  const engineers = m.integer("engineers", { lb: 0, ub: 20 });
  const budget = m.continuous("budget", { lb: 0, ub: 100000 });
  const rushDelivery = m.bool("rushDelivery");

  // Rule 1: Each engineer costs $8,000
  m.constraint(expr`8000 * ${engineers} <= ${budget}`, "budget_limit");

  // Rule 2: Customer requires rush delivery
  m.constraint(rushDelivery, "rush_required");

  // Rule 3: Rush delivery requires at least 8 engineers
  m.constraint(implies(rushDelivery, expr`${engineers} >= 8`), "rush_staffing_rule");

  // Rule 4: Board budget cap of $50,000 (Conflict!)
  m.constraint(expr`${budget} <= 50000`, "strict_board_budget_cap");

  // Rule 5: Innocent bystander rule
  m.constraint(expr`${engineers} >= 1`, "minimum_one_employee");

  // Run diagnosis
  const res = await m.check({ solver: "z3" });

  console.log(`Status: ${res.status}`);
  console.log("Z3 Unsat Core (scale-invariant):", m.conflicts);

  // Built-in HiGHS can also diagnose conflicts via single-solve L1 elastic slack relaxation:
  const highsDiag = await m.check({ solver: "highs" });
  console.log("HiGHS Elastic Repair Set:", highsDiag.conflicts);
}

diagnoseConflicts();

Open in Playground →

Practical Notes

• Z3 unsatCore vs. HiGHS Elastic Slack conflicts:
  • Z3 (m.check({ solver: "z3" })) performs logical assumption tracking and returns all four rules that jointly form the contradiction (budget_limit, rush_required, rush_staffing_rule, strict_board_budget_cap), while excluding the innocent minimum_one_employee rule.
  • HiGHS (m.check({ solver: "highs" })) solves a single $L_1$ elastic slack minimization problem ($\min \sum s_i$). Because relaxing rush_staffing_rule (or rush_required) requires a slack of only 1–2 units whereas relaxing strict_board_budget_cap requires a slack of 14,000 dollars, unweighted $L_1$ minimization naturally highlights the smallest-magnitude repair (rush_required) needed to restore feasibility.