Z3 SMT Solver Engine

Z3 is a theorem prover and Satisfiability Modulo Theories (SMT) solver developed by Microsoft Research. In WaSHI, Z3 provides advanced propositional logic reasoning and conflict diagnosis.

---

Installation

Z3 is provided as an optional peer dependency:

npm install z3-solver

---

When to Use Z3?

1. Unsat Core Conflict Diagnosis: When your MIP model is infeasible and you need to isolate which constraints are contradictory.
2. Boolean / Logical Formulations: When solving problems containing complex logical relations (implications, XOR, nested Boolean expressions).
3. Exact Mathematical Guarantees: Z3 can perform exact rational arithmetic without floating-point inaccuracies.

---

Basic Usage

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 Extraction (model.check())

Use await model.check() with Z3 to verify satisfiability and extract the conflicting subset of named constraints (conflicts / unsatCore) when a model is unsatisfiable:

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("Conflicting constraints:", result.conflicts); // or model.conflicts / model.unsatCore
  // ["req_A", "req_B"]
}

---

Browser Security Note

In browser environments, the Z3 WASM engine relies on pthreads and SharedArrayBuffer, which require cross-origin isolation headers (COOP / COEP). See the Cross-Origin Isolation Guide for detailed setup.

Runtime Failures and Thread Cleanup

If a Z3 worker encounters a fatal runtime error, pending operations on that instance reject with an error and the broken runtime is invalidated; subsequent solve() or check() calls automatically initialize a fresh Z3 runtime rather than misclassifying failures as Sat or Unsat.

To explicitly terminate Z3 pthread workers when tearing down a browser view or worker pool, call killZ3Threads() from @ohtaman/washi/solvers/z3.