Z3 SMT ソルバーエンジン

Z3 は Microsoft Research が開発した定理証明器・SMT（Satisfiability Modulo Theories）ソルバーです。WaSHI では、命題論理制約の解決と実行不可能モデルの競合診断（Unsat Core 抽出）に Z3 を利用します。

---

インストール

Z3 はオプションの peer dependency として提供されます：

npm install z3-solver

---

Z3 を選ぶべき場面

1. Unsat Core による矛盾制約の診断: モデルが実行不可能（Infeasible / Unsat）になった際、どの名前付き制約同士が矛盾しているかを特定したい場合。
2. 命題論理・ルールエンジンの定式化: 含意（implies）、排他的論理和（xor）、否定（not）などの論理式と算術制約が混在する問題を解く場合。
3. 厳密な有理数演算: 浮動小数点誤差のない厳密な充足性判定が必要な場合。

TIP

Z3（m.check()）と HiGHS（m.solve()）の使い分け: Z3 は充足可能性判定（m.check()）、セキュリティや業務ポリシーの形式検証、一般の線形不等式を前提とする含意（implies(expr`${x} <= 50`, y)）、およびスケールに依存しない unsatCore 抽出で最大の威力を発揮します。一方、数十〜数千変数の目的関数（コスト最小化・利益最大化など）を伴う数値的な LP / MIP / 凸 QP 最適化では、シンプレックス緩和と分枝限定法・切除平面を備えた標準搭載の HiGHS（m.solve()）の方が Z3.Optimize よりも圧倒的に高速です。両者を組み合わせ、「Z3 の m.check() でルール充足・矛盾診断を行い、HiGHS の m.solve() でコスト最適化を行う」ハイブリッド構成も実務で非常に有効です。

---

基本的な使い方

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

const model = new Model({ solver: "z3" });

const x = model.integer("x", { lb: 0, ub: 10 });
const y = model.integer("y", { lb: 0, ub: 10 });

model.constraint(expr`${x} + ${y} == 15`, "sum_15");
model.constraint(expr`${x} >= 8`, "x_at_least_8");

await model.solve();
console.log(`x = ${x.value}, y = ${y.value}`);

---

Unsat Core（矛盾コア）の抽出 (model.check())

await model.check() を使用すると、充足可能性を判定し、充足不能（"Unsat"）の場合に矛盾する名前付き制約の部分集合（conflicts / unsatCore）を取得できます：

const model = new Model({ solver: "z3" });
const a = model.continuous("a");

model.constraint(expr`${a} >= 10`, "req_A");
model.constraint(expr`${a} <= 5`, "req_B");

const result = await model.check();

if (result.status === "Unsat") {
  console.log("矛盾している制約:", result.conflicts); // または model.conflicts / model.unsatCore
  // ["req_A", "req_B"]
}

---

ブラウザ環境でのセキュリティ要件

ブラウザ環境では、Z3 WASM エンジンは pthreads と SharedArrayBuffer を使用するため、Cross-Origin Isolation（COOP / COEP ヘッダー）が必要です。設定手順の詳細は Cross-Origin Isolation 設定 を参照してください。

ランタイム障害時の復旧とスレッド終了

Z3 ワーカーでランタイムエラーが発生した場合、実行中の Promise は明示的に reject されて壊れたインスタンスは破棄されます（エラーが誤って Sat や Unsat に変換されることはありません）。次回の solve() または check() 呼び出し時には新しい Z3 ランタイムが再初期化されます。

ブラウザ画面のアンマウント時などに Z3 の pthread ワーカーを明示的に終了したい場合は、@ohtaman/washi/solvers/z3 からエクスポートされている killZ3Threads() を呼び出してください。