利かずの駒並べをSATでさっと解きたかった
利かずの駒並べをOR-ToolsのCP-SATソルバで解いてみました。 制約条件を工夫することでなんとか全3720通りの置き方を列挙できました。 ただ、そんなにさっとは解けないです。
利かずの駒並べのルールについては前回のエントリを参照してください。
CPへの帰着方法
位置 に玉／飛／角／……／歩がいるかどうかを表す
通りの変数を用意します。
以下では、玉が位置
にいるかどうかを
の要領で書きます。
また、
とします。
*1
この変数に以下の3つの制約を入れることで、利かずの駒並べを制約充足問題（CP）に帰着できます。
- 各駒を必要な枚数分配置する。すなわち、 \begin{align} \sum_{i,j} 玉_{i,j} &= 2, \\ \sum_{i,j} 飛_{i,j} &= 2, \\ &\vdots \\ \sum_{i,j} 歩_{i,j} &= 18. \end{align}
- 各マスには高々1枚しか駒を置けない。すなわち、 \begin{align} \sum_{p\in\mathcal{P}} p_{i,j} \leq 1. \qquad(\forall i, j) \end{align}
- 利きのあるマスには駒を置けない。すなわち、位置
にいる 駒
の利きが届くマスの集合を
とすると、 \begin{align} p_{i,j} = 1 \Rightarrow \forall p'\in\mathcal{P}, (i',j')\in E_{i,j}^{p}: p'_{i',j'}=0 \end{align}
数値実験
GoogleのOR-Toolsに
含まれるcp_modelを使用しました。
cp_model は制約充足問題のソルバで、CPをSATに帰着してさっと解くことができます。
コード
上記の制約条件をそのまま実装したところ計算に死ぬほど時間がかかったので、 飛び道具（飛、角、香）の探索が先に走るように制約を少し工夫しました。
実行結果
1
---
g pllll g
r
p psssp g
r
k ppppp p
n n
s p p p g
n p p
n pbpbp k
2
---
g pllll g
r
p psssp g
r
g ppppp p
n n
k p p p s
p p n
k pbpbp n
...（中略）
3720
---
g lllsl g
r
p psppp g
r
k pspsp p
n n
k p p p p
p p n
g pbpbp n
t= 232.79344301100002
4
Solutions found : 3720
232.8 秒で全 3720 通りの列挙に成功しました。 前のエントリで専用ソルバを作って全列挙した際は 0.18 秒だったので、 約1300倍の時間がかかってしまいました。
CP-SATくんは特に歩の配置に苦戦しているらしく、81 マスに 45 枚の歩を配置する問題は 時間がかかりすぎて解けませんでした。 専用ソルバでは劣化駒探索で歩の配置を高速に求めることができるので、実行時間に差が出たのかもしれません。
まとめ
利かずの駒並べは SAT ではあまりさっとは解けないです。さっと解きたいなら専用ソルバを作りましょう。
