本文へスキップ
トップに戻る
Ctrl
+
K
考えるコード ― 制約と最適化の冒険
検索
Ctrl
+
K
Z3
制約充足問題（CSP）― お弁当を食べ終わる順番を決めよう
Z3の使い方 ― 5つのステップで制約を解く
少ない枚数で払う ― Optimize で最適化する
マインスイーパー ― 数字のヒントから安全なマスを推理する
運動会の得点パズル ― 競技数が分からない問題を解く
10個の質問パズル ― 自己参照クイズを Implies で解く
24を作る ― 4つの数と演算子の組み合わせを探す
演算子を入れて99を作る ― 括弧の付け方を Z3 に探させる
ナイトツアー ― すべてのマスを1回ずつ訪れるルートを探す
ナンバーリンク ― 数字のペアを線でつなぐ
擬似乱数の予測 ―
rand()
のシードを Z3 で逆算する
グレーコード ― 1ビットずつ変化する数列を作る
CRC32を破る ― ハッシュ値から元のデータを作る
Z3 のデータ型 ― 式・型・関数宣言の関係を知る
Fixedpoint ― 再帰的なルールで到達可能性を解く
PySat
数独をSATで解く ― 「ちょうど1つ」をCNFで表す
ノノグラムを解く ― 位置変数でCNFを小さくする
四角に切れを解く ― マスと数字をブール変数で結ぶ
OrTools
CP-SATの紹介 ― SATの技術で解く制約プログラミング
CP-SATの基本API ― 制約を書くための道具一覧
ノノグラムを解く ― 開始位置を整数変数にする
箱詰めパズル ― 12種類のペントミノを詰める
サーキット・ツアー制約 ― 1本のループで順番を決める
スリザーリンク ― 格子点の回路として解く
ましゅ（Masyu）― 丸の制約を辺で書く
Yin-Yangパズル ― 色の連結を整数の番号で表す
ナンバーリンク ― 数字のペアを回路でつなぐ
巡回セールスマン問題 ― 距離が最小の回路を探す
Repository
Open issue
索引