Lab Assignment #1
8 queens problem
SAT vs ASP
This assignment consists in locating n=8 queens in a n x n square chessboard
so that they do not attack one each other. The image below
shows one of the possible arrangements for n=8:
What to do
We will encode the scenario both as a
SAT problem and as an ASP program.
- SAT: write a program in any programming
language of your choice (C, java, python, caml,
prolog, etc) that generates a propositional SAT
encoding of the 8 queens problem. This SAT encoding
will be a cnf file in format DIMACS, as explained in
the slides in classroom. For the SAT encoding, it
suffices with obtaining one solution or
arrangement of the queens. A second program will take
the SAT output (use clasp
as SAT solver) and generate a pretty printing of the
result. For instance, as a suggestion, the scenario
above could be displayed as:
. . . . . . Q .
. . Q . . . . .
. . . . . . . Q
. Q . . . . . .
. . . . Q . . .
Q . . . . . . .
. . . . . Q . .
. . . Q . . . .
- ASP: write an ASP encoding of the
same problem and use clingo
to generate solutions. In this case, the pretty
printing is not needed (assuming that the predicate
representation you choose is meaningful and readable).
Use clingo to obtain
all the solutions of the 8-queens problem. How
many solutions are there?
Assessment & delivery
The maximum grade for this exercise (1a)
is 0.65 points = 6.5% of the course. The deadline
for delivery is Friday, March
10th, 2017 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 describing how to compile the code for the SAT
interface programs. Regardless of the programming language
you choose, avoid using non-standard libraries.