OxiZ

A round-the-clock shift roster, solved in your browser. Toggle a constraint and the solver answers in tens of milliseconds. It speaks the same SMT-LIB language as Z3. The data never leaves this page.

Nothing is transmitted: not the constraints you set, not the roster that comes back. The solver runs entirely in your browser.

Shift board
Name	Mon	Tue	Wed	Thu	Fri	Sat	Sun
Sample A
Sample B
Sample C
Sample D
Sample E
Sample F

E = early shift D = day shift L = late shift N = night shift O = day off O◇ = requested day off

Presets

6 queens Magic square Pigeonhole XOR swap verification

You can edit a preset before running it.

Solver output (verbatim)

The output is the solver's standard SMT-LIB2 response, exactly as produced. Type (get-info :version) and the solver running here names itself.

oxiz	v— (Pure Rust, Apache-2.0)
target	wasm32-unknown-unknown
wasm size	1332 KB (gzip 494 KB)
last solve	—
decisions / conflicts	—
propagations / learned clauses	—
constraints (named assertions)	—
verdict	—
external requests	—
server round-trips	0
C / C++ / Fortran	0 bytes

External requests since the page finished loading: —

The external-request count starts once the wasm module has finished loading. Toggling constraints, solving, and running console scripts do not move it. One exception: Cancel restarts the solver, which re-fetches the same-origin worker chunk once, so the count rises by 1 — counted, not hidden. You can confirm all of this in your browser's Network tab.

Honest limits

Limit	What actually happens	Why
This is a simplified roster model, built for the demo	Many constraints of real 24/7 rostering are missing: skill mixes, overlapping time windows, month boundaries, fairness optimization, and more	Six people × seven days × ten constraints is just enough to show the SMT core loop — pick constraints, solve, pinpoint the conflict — and nothing else
The board is modeled with Bool variables	Written naively with Int variables, the same board takes the same solver about 26 seconds (over 80 seconds in wasm). This Bool version takes tens of milliseconds	SMT solve times change by orders of magnitude with the encoding. We measured both and shipped the fast one — the generated SMT-LIB2 is on this page for you to check
Solves are cut off by conflict count, not by time	When the limit is reached the answer is unknown (cut off). If a run still will not stop, Cancel restarts the entire solver	wasm32 has no clock, so OxiZ's wall-clock timeouts cannot fire. A conflict budget needs no clock, and a restart always works
The console is not a guarantee of every solver feature	Stepping into some features — quantifiers, for example — can crash the solver in the wasm build; it then restarts automatically	What is verified to run under wasm is the range this page uses: QF_UF / QF_LIA / QF_BV, plus model and unsat-core extraction. Everything beyond that is honestly labeled unverified
Nonlinear arithmetic	Nonlinear real arithmetic (QF_NRA) returns unknown. Nonlinear integer arithmetic (QF_NIA) is unaffected	The nonlinear solver (nlsat) is compiled out to keep the wasm small. QF_NIA is decided by static patterns and by model search verified outside nlsat, so removing nlsat does not change those answers
No solution enumeration, no optimization (MaxSMT)	Pressing Solve again on the same board gives the same answer	v1 does satisfiability and conflict pinpointing, nothing else. Determinism is itself verifiability: anyone can re-run this and get the same roster

Implementation code

// crates/oxiz-wasm/src/session.rs:84-90 — verbatim, the code running above
pub fn run_script(&mut self, script: &str) -> Result<String, OxizWasmError> {
    script::check_script(script)?;
    match self.ctx.execute_script(script) {
        Ok(lines) => Ok(serde_json::json!({ "ok": true, "lines": lines }).to_string()),
        Err(error) => Err(classify(&error)),
    }
}

This is the code running above, right now.