Z3 solver playground

Z3 is an SMT solver: give it variables and constraints over integers, reals, bit-vectors, arrays, strings and functions, and it finds values that satisfy them all (sat, with a model) or proves that none exist (unsat). That second answer is what makes it a theorem prover: to show a claim always holds, ask for a case where it fails, and unsat is the proof.

This page loads the real Z3 — the official z3-solver package, Z3 compiled to WebAssembly — from jsDelivr the first time you solve something. It is about 6.5 MB to download (35 MB uncompressed), cached by the browser afterwards.

How to use it

Turning Z3 on. Z3’s WebAssembly build runs on several threads, and browsers only allow that on a page that is cross-origin isolated, which needs two HTTP headers this site’s host (GitHub Pages) cannot send. Enable Z3 installs a small service worker that adds those headers for this page only — its scope is /tools/z3/; no other page on the site is touched — and reloads. After that Z3 loads when needed. Turn isolation off removes it. Where service workers are not available (some private windows, or this page inside another page), the puzzles still work with plain JavaScript search and say so on every answer; the SMT-LIB editor needs Z3.

Puzzles. Each one builds an SMT-LIB script from what you enter, solves it, decodes the model back into an answer, checks the answer independently, and shows the script (Open in the SMT-LIB editor to change it):

Sudoku — type a grid or pick one (including Arto Inkala’s "hardest"); Solve and check it is unique adds one assertion that rules out the first solution and asks again.
N-queens — any N up to 40; Count all solutions finds them one by one, blocking each in turn (92 for eight queens).
SEND + MORE = MONEY — or any word sum; Find all solutions.
Magic squares — 3×3, 4×4, 5×5, with numbers you fix first; Another one excludes the squares found so far.
Scheduling — tasks with durations, people, dependencies and deadlines; Z3’s optimiser (minimize) finds the earliest finish, drawn as a chart, with a simple lower bound for comparison.
Timetabling — exams and the students taking them, into as few slots as possible.

Bit-vectors. A few lines of a C-like language over 8-, 16-, 32- or 64-bit integers that wrap on overflow: name = expression, assume condition, prove condition. Z3 either proves the claim for every input or gives a counterexample, which the page re-runs step by step. Examples: x & (x - 1) clears the lowest set bit; the power-of-two test that forgets zero; the binary-search midpoint (lo + hi) / 2 that overflowed in Java’s library for nine years, and its fix; abs(INT_MIN); XOR swap; x >> 1 versus x / 2; branchless min; signed overflow. Signedness picks bvsdiv/bvudiv, bvashr/bvlshr and signed or unsigned comparisons. Division by zero follows SMT-LIB (x / 0 is all ones unsigned), not C’s undefined behaviour.

SMT-LIB. Write any SMT-LIB 2 script and run it (Ctrl/⌘+Enter). Results show as readable blocks — sat/unsat, models as a table, get-value, objectives, errors with line numbers — or as Z3’s raw output. Bit-vectors read as hex, unsigned and signed; rationals with a decimal. Examples cover integers, push/pop, non-linear reals, bit-vectors, uninterpreted functions, arrays, quantifiers, optimisation, strings and unsat cores. Each run uses a fresh solver; the timeout applies per check-sat, and Stop interrupts a long search.

History keeps the last 60 scripts run in the editor. Share link carries the open puzzle and its settings, the program and the editor text.

For plain SAT on clauses (with the algorithm shown step by step) see Boolean logic; for the maths behind some puzzles, the CAS.

Limits

Z3 needs cross-origin isolation (above). In Safari the isolated page also blocks cross-origin files that don’t opt in, such as the site’s analytics, on this page only.
Some problems never finish — non-linear integer arithmetic is undecidable in general — and not every part of Z3 checks for a stop request. If Stop does not help, reload the page.
The JavaScript fallback has no scheduling (that needs the optimiser) and only tries every input for bit-vector programs with at most 2²² input combinations.

Browser support

Chrome, Edge, Firefox and Safari (recent versions) with service workers and WebAssembly threads.

Privacy

Everything runs in the page. Z3 (MIT licence) is downloaded from cdn.jsdelivr.net when first needed. The service worker only adds headers to this page’s own requests; it does not store or send anything. Settings and history are kept in this browser’s local storage.