Binairo Puzzle

Бинаиро Головоломка

Введение

Этот проект заключается в решении головоломки Бинаиро (см. здесь онлайн-игру), также называемой Такузу, и описываемой следующим образом. У нас есть сетка из nxn ячеек, которая может содержать белый или черный кружок. В исходной конфигурации предусмотрены некоторые значения ячеек, а остальные должны быть заполнены кружками в соответствии со следующими правилами:

• Каждая строка и каждый столбец должны содержать одинаковое количество кружков каждого цвета, то есть n/2 экземпляров каждого случая.

• Не может быть более двух последовательных кругов одного цвета в любом направлении (вертикальном или горизонтальном).

• Не может быть двух строк или двух столбцов с одинаковой конфигурацией.

Пример начальной конфигурации и соответствующее решение можно увидеть ниже.

Выполнение

Он закодирует сценарий как в виде задачи SAT, так и в виде программы ASP.

Для этого используется файл ASCII с исходной сеткой, в которой каждая ячейка содержит символ: «0» (белый кружок), «1» (черный кружок) или «.». (пустая ячейка для заполнения). В первой строке записано четное число n>=2, указывающее количество строк и столбцов (у нас квадратная сетка). Например, пример на рисунке выше будет представлен как:

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

Эта программа создаст файл DIMACS и выполнит внешний вызов clasp , когда она использует SAT, или clingo, когда она использует ASP для получения решения. Он также декодирует выходные данные и печатает полное решение следующим образом:

 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