Binairo Puzzle

ビナイロパズル

導入

このプロジェクトは、Takuzu とも呼ばれる Binairo パズル (ここではオンライン ゲームを参照) を解くことで構成されており、次のように説明されています。白丸または黒丸を含む nxn 個のセルのグリッドがあります。初期設定ではいくつかのセル値が提供され、残りは次のルールに従って円で埋める必要があります。

• 各行と各列には、各色の同じ数の円、つまり各ケースの n/2 インスタンスが含まれている必要があります。

• どの方向 (垂直または水平) においても、同じ色の円を 2 つ以上連続して配置することはできません。

• 同じ構成を 2 つの行または 2 つの列にすることはできません。

初期構成と対応するソリューションの例を以下に示します。

実装

シナリオは SAT 問題と ASP プログラムの両方としてエンコードされます。

これは、各セルに文字「0」(白丸)、「1」(黒丸)、または「.」が含まれる初期グリッドを含む ASCII ファイルを取得します。 (空のセルに入力します)。最初の行には、行と列の数を指定する偶数 n>=2 が含まれています (正方形のグリッドがあります)。たとえば、上の図の例は次のように表されます。

 6
......
.11.0.
01....
....00
.1....
0..1..

このプログラムは DIMACS ファイルを生成し、SAT を使用する場合はclaspへの外部呼び出しを行い、ASP を使用する場合はclingo を呼び出して解決策を取得します。また、次のように出力をデコードし、完全なソリューションを出力します。

 100110
011001
010011
101100
110010
001101

実行

デフォルトでは ASP が使用され、サンプル フォルダーにはさまざまなサイズ (6、8、10、14、20) の一連のベンチマークが含まれています。domX.txt は入力ファイル、solX.txt はそれに対応するソリューションです。

 ./binairo.py [-h] [-a] [-c input] input

-h            show this help message and exit
-a            use ASP to solve
-c            compare the result with this file
-input        route of the binairo puzzle instance