「必ず解ける」を保証する仕組み

SATソルバーを使用しています（SATの説明は別記事予定）
行列のマスが地雷かを変数で表現します。
がTrueならそのマスに地雷があることを、Falseなら地雷がないことを表します。
下記のようにルールをSATの条件として統一して扱うことができます

地雷数

総地雷数をとして盤上の全マス目についてで表します
ここではがTrueなら、Falseならとして和を取ることを表します
単純なSATでは和はそのまま表現できないので工夫が必要でした（整数和をSATでエンコード）

通常のヒント

画像の例ではを満たすがあるかを調べればよいです

特殊ルール

「縦横斜めに一直線に３個地雷が並ばない」

これは３連続のマス目をすべて列挙してその中のの和が3でないことを制約とします
上記とは異なり和が~で「ない」ことをSATで表現する必要があります

「すべての地雷が縦横につながっている」

マス目をノードとしその上下左右のマスとの間にエッジがあるグラフを考えます
地雷の総数をとしてこのグラフにサイズの連結サブグラフがあるかを制約にします
グラフの条件もSATにエンコードする必要がありました

「すべての地雷が縦横でペアになっている」

縦横２マスを総列挙してそれぞれの和がかになるという制約で表します