Assignment 3

In this assignment is to use minisat to solve some constraint satisfaction problems. Even though the inputs can be quite large and complex-looking, minisat can usually solve large problems more quickly than csp.py.

Installing and Using minisat

minisat is a popular SAT solver that you can install in Ubuntu Linux with this command:

$ sudo apt install minisat

The lecture notes contain examples of how to properly format the input CNF file. You may also find this user guide helpful.

For example, if you have a properly formatted CNF file named graph2.txt, then you run minisat like this:

$ minisat graph2.txt out

When the solver finishes, the text file out will contain either a satisfying assignment (a list of positive and negative numbers ending with 0), or UNSAT if there is no satisfying assignment.

Question 1 (N-queens with SAT)

Write a Python called make_queen_sat(N) that generates a SAT sentence (as a Python string) that, when satisfied, will be a solution to the N-queens problem.

Also, write a function called draw_queen_sat_sol(sol) that takes the output of minsat as a string and draws the resulting N-queens solution on the screen (using print). This only needs to work for solutions of up to size N=40; it can just print a message like “too big: N must be less than 40” if N > 40. The string sol is the contents of the output file from minisat, i.e. either a list of positive and negative numbers ending with a 0, or UNSAT. If sol is UNSAT, then draw_queen_sat_sol should print a message like “no solution”.

Put all the code you need for this question into a file called a3_q1.py.

Using make_queen_sat (and draw_queen_sat_sol to help with visualizing results), run an experiment to determine the max value for N that minisat can solve for in 10 seconds, or less. Call this value MAX_N.

Note: If 10 seconds seems like the wrong amount of time to get useful results, then you can change it to something else. Whatever time you use, make sure to clearly state it in your spreadsheet below.

In an Excel worksheet named a3_q1.xlsx (e.g. use Excel, or Google Sheets to make it), for each value of N from 2 to MAX_N, tabulate and plot the amount of time it takes for minisat to solve the problem. Make your results neat and easy to read.

In your spreadsheet, please include any other helpful or relevant information.

Question 2 (Ice Breaker Revisited)

Use minisat to solve the Ice Breaker problem from assignment 2. We will use the same problem description, rules, and graph format as in assignment 2.

Create a function called make_ice_breaker_sat(graph, k) that takes a friendship graph as input (see assignment 2) and a positive integer \(k\) representing the number of possible teams (i.e. each node can be one of \(k\) colors). It returns, as a Python string, an encoding as a SAT problem that can be used as input to minisat. It is your job to design a SAT encoding, and to implement it in make_ice_breaker_sat.

Next, write a function called find_min_teams(graph) that uses minisat to find the (exact) minimum number of teams the people can be divided into such that no team has any friends (teams of 1 are permitted). find_min_teams(graph) should return a single integer: the (exact) minimum number of teams.

Note that you can run command line commands in Python using os.system, e.g.:

import os

os.system('minisat some.graph some.out')

You could then open the output file some.out to check the results. See the Python documentation for other ways to get the results of commands.

Put all the Python code you need for this question into a file called a3_q2.py.

Now do some experiments with random graphs. For \(n = 1000\), and for the nine values \(p=0.1, 0.2, \ldots, 0.9\), collect the following data:

  • the average number returned by find_min_teams
  • the average solving time

These are averages, so for each value of \(p\) you should create and solve multiple instances (e.g. maybe 10 for each value of \(p\)).

Note: If \(n=1000\) seems to be too big (or too small) for your computer, then you can use some other value of \(n\). Try to make it as big as possible. Whatever value you end up using, make sure to clearly state it in your spreadsheet below.

In an Excel worksheet named a3_q2.xlsx (e.g. use Excel, or Google Sheets to make it), tabulate and plot your data. Make your results neat and easy to read.

In your spreadsheet, please include any other helpful or relevant information.

What to Submit

For this assignment you should submit:

  • a3_q1.py: contains make_queen_sat(N), draw_queen_sat_sol(sol) (and whatever helper functions they rely on)
  • a3_q1.xlsx
  • a3_q2.py: contains make_ice_breaker_sat(graph, k), find_min_teams(graph) (and whatever helper functions they rely on)
  • a3_q2.xlsx

Use the exact file and function names — otherwise marking scripts might give you 0!

As with previous assignments, use only code that you have written yourself. The only exceptions are that you may use any code from the standard Python 3 library, or from the textbook code from Github (please don’t make any modifications to the textbook code).

Make the spreadsheets beautiful, informative, and easy to read. Be sure to include helpful descriptive statistics like the min, max, average, and median values when it makes sense to do so. You are encouraged to include helpful or informative graphs of your data. Spelling, grammar, and neatness count!

Put all the files needed to re-run your questions into a single .zip archive named a3.zip, and submit it on Canvas before the due date listed there.

Hints

  • Be very careful with the SAT encodings! It is easy to forget a constraint or make little mistakes that cause your encoding to be wrong. Be sure to test your code on small examples to ensure it is correct.
  • Be careful: minisat does not allow 0 to be used as a variable.