# 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` | <ul><li><a href="https://washi.ohtaman.dev/demo/?preset=conflict_diagnosis_unsat">Open in Playground</a></li><li><a href="https://github.com/ohtaman/washi/blob/main/examples/node/05-unsat-core-diagnosis.ts">Source Code</a></li></ul> |

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

<CodeRunner preset="conflict_diagnosis_unsat">

```typescript
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();
```

</CodeRunner>

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