CS 444 - Problem Solving in Prolog

Due by Blackboard turn in by 11:59pm on Monday, November 22.

This programming assignment is to be done in teams of two. By default your team is the same as for the first assignment. If two people wish to swap teams, they should both email the instructor.

In class on Nov. 4th we talked about Latin Squares, also known as quasigroups, and how they have many applications in science and engineering. In this project, you will solve quasigroup completion problems (QCP) in two different ways: (i) by writing a solver in Prolog and (ii) by using Prolog to generate a propositional SAT problem representing the QCP, and then solving the SAT problem with an off-the-shelf SAT solver. There are three parts to the assignment:

Part 1: Write a Prolog program that generates and prints out 10 x 10 quasigroups. Use the integers 0 to 9 to represent the different colors. Calling the predicate 'solve' should print out a solution as a 10 x 10 table. It should be possible to enter ';' and return to get another solution, and so on.

The simplest Prolog program you could write would simply modify the magic square program we showed in class. This is fine, but has a couple of drawbacks:

If you have time after completing the rest of the assignment, you might try to find a more elegant and/or faster approach. For example, you could represent the square by a list of lists (i.e., a list of rows, where each list is a list of numbers). Can you use the built-in 'permutation' predicate? Or, you could represent the board using a predicate, e.g. 'p(row,column,color)', and then keep track of what squares have been filled in using 'assert' and 'retract'.

Side remark: You can define a version of 'assert' that automatically retracts what was asserted when backtracked over as follows:


Part 2: Modify your program so that it solves quasigroup completion problems, i.e., ones where some of the squares are specified in advance. Test your program on (at least) the following three instances:

The first two problems have a solution, the third problem has no solution. The problems are specifed by a series of lines containing three integers:

The first row or column is numbered 1 (not 0). Your program does not have to be able to read these files in, it is fine to "hard wire" these problems into your program (or into three different versions of your program).

Part 3: Modify the program schema.pl to make it generate SAT encodings of QCPs. The program begins with instructions on how to use it to generate a propositional CNF problem, and how to use it to interpret the solution from a SAT solver relative to a particular problem encoding.

Test on the same three QCPs from Part 2. For the solvable instances, solve the generated problems using my implementation of Walksat, which you can download here. For the unsat instance, use the solver Minisat, which can be downloaded here. Finally, also try solving the instances using your solution to the first programming project.

Write up: Write up a short report that includes