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.

TIP

Z3 (m.check()) vs. HiGHS (m.solve()): Z3 excels at satisfiability checking (m.check()), formal policy verification, general inequality implications (implies(expr`${x} <= 50`, y)), and scale-invariant unsatCore extraction. For numerical LP, MIP, or Convex QP optimization with objective functions over tens or hundreds of variables, use the built-in HiGHS solver (m.solve()), whose simplex relaxations and branch-and-bound cutting planes are orders of magnitude faster than Z3.Optimize. Or combine both in a hybrid pipeline: verify/diagnose rules with Z3 m.check(), then optimize costs with HiGHS m.solve().

---

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.