COOLJAPAN Playground github.com/cool-japan

OxiZ

シフト表が、ブラウザの中で解ける。制約を選ぶと Z3 と同じ言葉を話す SMT ソルバが数十ミリ秒で答えを返す。データはこのページから一歩も出ない。

入力した条件も、出来上がったシフト表も、送信されません。解いているのはあなたのブラウザです。

名前月火水木金土日
見本A
見本B
見本C
見本D
見本E
見本F

早=早番 日=日勤 遅=遅番 夜=夜勤 休=休み 休◇=希望休

oxizv— (Pure Rust, Apache-2.0)
targetwasm32-unknown-unknown
wasm size1332 KB (gzip 493 KB)
直近の求解—
決定 / 競合—
伝播 / 学習節—
制約 (named assertions)—
判定—
external requests—
server round-trips0
C / C++ / Fortran0 bytes

ページ読込後の外部リクエスト: — 件

外部リクエストの計測は、wasm の読み込みが完了した時点から開始しています。条件の切り替え・求解・コンソールの実行を行っても、この数は動きません。ただし「中止する」でソルバを再起動した場合だけ、同一オリジンの worker チャンクを 1 回取り直すため 1 件増えます（隠さずに数えています）。開発者ツールの Network タブでも確認できます。

正直な制約

制約実際に何が起きるかなぜ
これはデモ用に簡略化したシフトモデルです実務のシフト作成にある多くの条件（スキルの組合せ・時間帯の重なり・月またぎ・公平性の最適化など）は入っていません6人×7日×10種の制約で「制約を選ぶ→解く→衝突を特定する」という SMT の中核だけを見せるためです
盤面のモデリングは Bool 変数で行っています同じ盤面を Int 変数で素直に書くと、同じソルバでも解くのに約 26 秒（wasm では 80 秒超）かかります。この Bool 版は数十ミリ秒ですSMT はモデリング次第で速度が桁で変わります。実測して速い方を選びました（生成された SMT-LIB2 はページ上で確認できます）
求解の打ち切りは時間ではなく競合回数で行います上限に達すると unknown（打ち切り）と答えます。それでも止まらない場合は「中止する」がソルバごと再起動しますwasm32 には時計がなく、oxiz の時間タイムアウトは動きません。回数上限は時計いらずで、再起動は確実です
コンソールはソルバ全機能の保証ではありません量化子など一部の機能に踏み込むと、wasm 版ではソルバが落ちて自動再起動することがありますwasm で実行検証済みなのはこのページが使う範囲（QF_UF / QF_LIA / QF_BV とモデル・コア取得）です。それ以外は正直に「未検証」です
非線形算術非線形実数算術（QF_NRA）は unknown を返します。整数の非線形（QF_NIA）は影響を受けませんサイズ最適化のため、非線形ソルバ（nlsat）を除いてビルドしています。QF_NIA は静的なパターンと、nlsat の外で検証されるモデル探索で決まるため、除いても答えは変わりません
別解の列挙・最適化 (MaxSMT) はありません「解き直す」を押しても同じ盤面は同じ答えになりますv1 は充足判定と衝突特定に絞りました。決定的であること自体が検証可能性です

実装コード

// 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)),
    }
}

これがいま上で動いているコードです。