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