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:

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