Dominosa puzzle

This assignment consists in solving the Dominosa puzzle (see Simon Thatham's online game) described as follows. Someone has arranged all the domino tiles in a grid of 8 x 7 of squares (half tiles) as in the right image below. We use digits instead of the usual domino dotted images, so we have all tiles from (0,0) (0,1) ... up to (6,6). However, the initial state (left image below) only shows the numbers in the grid but not the correspondence to their tiles, which is precisely what we must find out.

Initial state	Solved puzzle: all tile arrangements are unvealed

The puzzle can be parameterized by the number n of digits, from 0 to n-1, being the usual domino game the case n=7.

Exercise (combinatorics): prove that for n different digits we can always arrange all the corresponding tiles in a grid of (n+1)*n digits. For instance, in the case of, we have a grid of n=8*7.

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

1. SAT: write a program called dominosa in any programming language of your choice (C, java, python, caml, prolog, etc). This program can be used in two ways.
   Solving mode: dominosa <inputfile>
   This takes an ASCII file with the grid of digits. The input format will be like the following for the example above:
   
   

   7 6 0 6 6 4 4 1 1 3 5 2 1 2 2 3 0 3 4 1 2 3 0 4 4 0 2 0 2 2 0 3 1 5 4 1 5 1 3 5 5 5 5 6 5 2 0 0 6 6 6 6 4 3 4 1 3

   
   where the first number is the value n=7 and, after that, we have n*(n+1) digits separated by spaces or intros. 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 tile directions as follows:
   
   

   ><vv><>< vv^^><vv ^^><><^^ vvvv><vv ^^^^><^^ ><><v><v ><><^><^

   where we use the notation:
      >< - represents the location of an horizontal tile and 
   
      v  - represents the location of a vertical tile
      ^
   
   Generator mode: dominosa -g <n> (removed)
   
   
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 (from n=2 to 10), where domN.txt is the input file and solN.txt its corresponding solution, being N a pair of digits representing the number n of different symbols.

If you want to push it forward, file examples2.zip contains larger benchmarks domN.txt, all of them correctly formed, but for which more than one solution may exist. Accordlingly, files solN.txt contain one of the possible solutions in each case. To check that another potential solution is correct you can use the python program checker.py as, for instance, in:

checker.py dom30.txt sol30.txt

Assessment & delivery