Binairo Puzzle

比內羅拼圖

介紹

該專案旨在解決 Binairo 難題（請參閱此處的線上遊戲），也稱為 Takuzu，描述如下。我們有一個 nxn 個單元格的網格，其中可能包含一個白色圓圈或一個黑色圓圈。初始配置提供了一些單元格值，其餘的必須根據以下規則用圓圈填充：

• 每行和每列必須包含相同數量的每種顏色的圓圈，即每種情況有 n/2 個實例。

• 在任何方向（垂直或水平）上不能有超過 2 個相同顏色的連續圓圈。

• 不能有兩行或兩列具有相同的配置。

初始配置範例和相應的解決方案如下所示。

執行

它將場景編碼為 SAT 問題和 ASP 程式。

這需要一個帶有初始網格的 ASCII 文件，其中每個單元格包含一個字元：“0”（白色圓圈）、“1”（黑色圓圈）或“.” （要填滿的空白儲存格）。第一行包含一個偶數 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