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, c } 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(c`${x} + ${y} == 15`, "sum_15");
model.constraint(c`${x} >= 8`, "x_at_least_8");

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

---

Unsat Core Extraction

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

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

await model.solve({ computeUnsatCore: true });

if (model.status === "Infeasible") {
  console.log("Conflicting constraints:", model.conflicts); // or model.unsatCore
  // ["req_A", "req_B"]
}

---

Browser Security Note

In browser environments, the Z3 WASM engine relies on SharedArrayBuffer and requires cross-origin isolation. See the Cross-Origin Isolation Guide for detailed setup.