Lab Assignment #1

8 queens problem



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:

8 queens

What to do

We will encode the scenario both as a SAT problem and as an ASP program.
  1. 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 . . . .

  2. 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.

Maintained by Pedro Cabalar. Last update 22/2/2017