Binairo Puzzle

Quebra-cabeça Binário

Introdução

Este projeto consiste na resolução do puzzle Binairo (veja aqui um jogo online), também denominado Takuzu, e descrito a seguir. Temos uma grade de células nxn que pode conter um círculo branco ou um círculo preto. A configuração inicial fornece alguns valores de células e o restante deve ser preenchido com círculos de acordo com as seguintes regras:

• Cada linha e cada coluna devem conter o mesmo número de círculos de cada cor, ou seja, n/2 ocorrências de cada caso.

• Não pode haver mais de 2 círculos consecutivos da mesma cor em qualquer direção (vertical ou horizontal).

• Não pode haver duas linhas ou duas colunas com a mesma configuração.

Um exemplo de configuração inicial e a solução correspondente pode ser visto abaixo.

Implementação

Ele codificará o cenário tanto como um problema SAT quanto como um programa ASP.

Isso leva um arquivo ASCII com a grade inicial onde cada célula contém um caractere: '0' (um círculo branco), '1' (um círculo preto) ou '.' (uma célula vazia a ser preenchida). A primeira linha contém um número par n>=2 especificando o número de linhas e colunas (temos uma grade quadrada). Por exemplo, o exemplo na imagem acima seria representado como:

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

Este programa irá gerar um arquivo DIMACS e fazer uma chamada externa para clasp quando usar SAT ou clingo quando usar ASP para obter uma solução. Ele também decodificará a saída traseira e imprimirá a solução completa da seguinte maneira:

 100110
011001
010011
101100
110010
001101

Execução

Por padrão, utiliza ASP e a pasta de exemplos contém um conjunto de benchmarks de diferentes tamanhos (6, 8, 10, 14, 20), onde domX.txt é o arquivo de entrada e solX.txt sua solução correspondente.

 ./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