Lab Assignment #1
Binairo puzzle
SAT vs ASP
Introduction
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:
- Each row and each column must contain the same
number of circles of each color, that is, n/2
instances of each case.
- There cannot be more than 2 consecutive circles of
the same color in any direction (vertical or
horizontal).
- 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
|
What to do
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
The maximum grade for this exercise is 25
points = 25% of the course. The deadline for
delivery is Friday, November
11th, 2022 using the MOODLE assignment.
Exercises can be made by groups of 2 students at most. If
so, only one student is required to deliver the files in
moodle, but all source files must contain the names of the
two group members.
Delivery: upload all files in a .zip including a
README.txt with the student names and any additional
comment you consider relevant.
|
|
|