# 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 guidehelpful.

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 kk representing the number of possible teams (i.e. each node can be one of kk 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=1000n=1000, and for the nine values p=0.1,0.2,…,0.9p=0.1,0.2,…,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 pp you should create and solve multiple instances (e.g. maybe 10 for each value of pp).

**Note**: If n=1000n=1000 seems to be too big (or too small) for your computer, then you can use some other value of nn. 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 Canvasbefore 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.

**程序代写代做C/C++/JAVA/安卓/PYTHON/留学生/PHP/APP开发/MATLAB**

本网站支持 Alipay WeChatPay PayPal等支付方式

**E-mail:** vipdue@outlook.com **微信号:**vipdue

如果您使用手机请先保存二维码，微信识别。如果用电脑，直接掏出手机果断扫描。