制約矛盾の診断 (Z3 Unsat Core)

問題クラス	ソルバー	主な API	リンク
実行不能 (Infeasible) 診断・Unsat Core	Z3 (@ohtaman/washi/solvers/z3)	m.integer(), m.continuous(), implies(), m.constraint(), expr, m.check(), m.conflicts	Playground で開く ソースコード

複数の業務ルールや数値制約が互いに矛盾して実行可能解が存在しない（Unsat）場合、名前付き制約の中から矛盾を引き起こしている制約の部分集合（Unsat Core。最小性は保証されません）を Z3 で抽出します。

矛盾が発生するシナリオ

ある開発チームが顧客プロジェクトの要員計画を立てています：

1. エンジニア1名あたり $8,000 のプロジェクト予算を消費する（budget_limit）。
2. 顧客から特急納品が要求されている（rush_required）。
3. 特急納品には最低 8 名のエンジニア配置が必須である（rush_staffing_rule）。
4. 役員会からプロジェクト予算の上限 $50,000 が厳命されている（strict_board_budget_cap）。
5. 労働基準により最低 1 名の社員を配置する必要がある（minimum_one_employee）。

ここで以下の矛盾が生じていることに注目してください：

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

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");

  // ルール 1: エンジニア1名あたり $8,000 のコスト
  m.constraint(expr`8000 * ${engineers} <= ${budget}`, "budget_limit");

  // ルール 2: 顧客が特急納品を要求
  m.constraint(rushDelivery, "rush_required");

  // ルール 3: 特急納品には最低 8 名のエンジニアが必要
  m.constraint(implies(rushDelivery, expr`${engineers} >= 8`), "rush_staffing_rule");

  // ルール 4: 役員会による予算上限 $50,000（矛盾の原因！）
  m.constraint(expr`${budget} <= 50000`, "strict_board_budget_cap");

  // ルール 5: 矛盾とは無関係なルール
  m.constraint(expr`${engineers} >= 1`, "minimum_one_employee");

  // 競合診断を実行
  const res = await m.check({ solver: "z3" });

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

  // 標準搭載の HiGHS でも単一 solve の L1 弾性スラック緩和で競合診断が可能:
  const highsDiag = await m.check({ solver: "highs" });
  console.log("HiGHS Elastic Repair Set:", highsDiag.conflicts);
}

diagnoseConflicts();

Playground で開く →

実務上のポイント

• Z3 の unsatCore と HiGHS の弾性スラック診断 (conflicts) の違い:
  • Z3（m.check({ solver: "z3" })） は論理的な仮定追跡を行い、無関係な minimum_one_employee を除外したうえで、矛盾を構成する4つのルール（budget_limit, rush_required, rush_staffing_rule, strict_board_budget_cap）を単位スケールに依存せず抽出します。
  • HiGHS（m.check({ solver: "highs" })） は単一 solve の $L_1$ 弾性スラック最小化（$\min \sum s_i$）を解きます。予算上限を $14,000 緩和するよりも特急要件・人数要件を 1〜2 単位緩和する方がスラック総和が小さいため、重みなし $L_1$ 最小化では「最小の数値変更で実行可能に戻せる修復箇所（rush_required）」が優先して提示されます。