はじめに 初投稿かつn番煎じです 数独について 数独とは ↑こういうやつ - 3×3のブロックに区切られた 9×9の正方形の枠内に1〜9までの数字を入れるペンシルパズルの一つ - ナンプレともいう https://ja.wikipedia.org/wiki/数独 数独のルール 空いているマスに1〜9のいずれかの数字を入れる 縦・横の各列及び、太線で囲まれた3×3のブロック内に同じ数字が複数入ってはいけない Z3について Z3とは Microsoft Research が開発したSMTソルバ MITライセンス https://github.com/Z3Prover/z3 SMTソルバとは 一階述語論理式の充足可能性を判定してくれる 充足可能(SAT)の場合は充足割り当て解の一つを出力してくれる 充足不可(UNSAT)の場合は出してくれない(そりゃそうだ) 解いてみる 準備 githubからz
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く