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

We will encode the scenario both as a SAT problem and as an ASP program.

1. SAT: write a program called binairo in any programming language of your choice (C, java, python, caml, prolog, etc) and used as:
   
   binairo <inputfile>
   
   This takes an ASCII file <inputfile> with the initial grid where each cell contains a character: '0' (a white circle), '1' (a black circle) or '.' (an empty cell to be filled). The first line contains an even number n>=2 specifying the number of rows and columns (we have a square grid). For instance, the example in the picture above would be represented as:
   

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

   
   Your program will generate a DIMACS file (as explained in class) and make an external call to clasp to get a solution. It will also decode back the clasp output and print the complete solution as follows:
   

   100110 011001 010011 101100 110010 001101

   
   
2. ASP: write an ASP encoding of the same problem and use clingo to solve the puzzle. In this case, the pretty printing is not needed (assuming that the predicate representation you choose is meaningful and readable) but you will need an extra program to transform the input files into ASP facts for the representation you choose.

File examples.zip contains a set of benchmarks of different sizes (n=6,8,10,14,20), where domX.txt is the input file and solX.txt its corresponding solution.

Assessment & delivery