Binairo puzzle

This assignment consists in solving the Binairo puzzle (see here an online game), also called Takuzu, and described as follows. We have a grid of n x n cells that may contain a white circle or a black circle. The initial configuration provides some cell values and the rest must be filled with circles according to the following rules:

1. Each row and each column must contain the same number of circles of each color, that is, n/2 instances of each case.
2. There cannot be more than 2 consecutive circles of the same color in any direction (vertical or horizontal).
3. There cannot be two rows or two columns with the same configuration.
   

An example of initial configuration and the corresponding solution can be seen below.

Initial configuration	Solved puzzle

Step 1. Each input instance is an ASCII file containing a squared grid (n x n) with the following format. The file contains n lines (the rows) and each line contains n characters (the columns) ended by a newline. Each cell contains a character: '0' (a white circle),'1' (a black circle) or '.' (an empty cell to be filled). For instance, the example in the picture above would be represented as:

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

In the compressed file examples.zip you will find several input domains of different sizes (n=6,8,10,14,20), where domX.txt is the input file and solX.txt its corresponding solution.

Step 2. Use the program encode.py to transform each input ASCII file into a logic program containing facts. For instance:

python3 encode.py < dom06.txt > domain.lp

will transform the example above into the set of facts:

cell(1,1,1). cell(1,2,1). cell(1,4,0). cell(2,0,0). cell(2,1,1). cell(3,4,0). cell(3,5,0). cell(4,1,1). cell(5,0,0). cell(5,3,1). dim(6). #const n=6.

where "cell(X,Y,V)" means that cell in row X and column Y contains value V (0 or 1).

Step 3. Encode the binairo problem in clingo in a file called binairo.lp. You can use

clingo 0 binairo.lp domain.lp

to obtain all the answer sets. You should check that each puzzle should have a unique solution. To display the puzzle solution as an ASCII file (as those included in the examples) you can use instead the program decode.py as follows:

python3 decode.py binario.lp domain.lp

Assessment & delivery