Constraint Satisfaction

Due:

11:00pm, Friday November 12, 2021

Description

Write a program that reads a graph file (detailed below) and prints to standard out a graph-coloring constraint satisfaction problem specified in SMT-LIB v2 format.

A graph file has the following format (source):

K=21
32 --> 6 7 8 0 1 2 
33 --> 6 7 8 0 1 
34 --> 7 8 0 6 35 36 37 38 39 
35 --> 34 8 0 7 36 37 38 39 1 
36 --> 34 35 0 8 37 38 39 1 6 
37 --> 34 35 36 0 38 39 1 6 7 
38 --> 34 35 36 37 
39 --> 35 36 37 34 1 6 7 8 
3<->32 2<->33 1<->34 6<->35 7<->36 8<->37 0<->38 34<->1 35<->6 36<->7 37<->8 39<->0 

The first line indicates a number of pre-colored nodes. In this case with K=21, there are 21 nodes numbered 0 to 20 that each have a distinct color.

The lines containing --> are interference edges. For example, this line

33 --> 6 7 8 0 1 

indicates that node 33 interferes with nodes 6, 7, 8, 0 and 1. This means that node 33 cannot have the same color as any of its interfering nodes.

The final line indicates nodes that must be the same color. For example, 3<->32 indicates that node 3 and node 32 must be the same color.

The last line that your program should output is:

(check-sat)

That is, we are only interested whether a given graph is satisfiable or not. Note that you may want to get the model when you are testing your program, but you should remove that from your program before submitting.

You can run your file with z3 as follows:

    ~schwesin/bin/z3 <(./project3 <graph file>)

where project3 is an executable file and <graph file> is path to a graph file.

Getting the Assignment

The starter code for the assignment is on the Linux server at the path:

/export/home/public/schwesin/csc447/projects/project3-handout

Turning in the Assignment

You must turn in the following files:

1. project3.x
2. README

The README file should be a plain ASCII text file (not a Word file, not an RTF file, not an HTML file) describing your design decisions. One or two English paragraphs should suffice. Spelling, grammar, capitalization and punctuation all count.

To submit the assignment, execute the command:

    make submit

from within the assignment directory.

Grading Criteria

Grading (out of 100 points):

• 70 points — Specification
  • 70 points — meets the specification
  • 40 points — partially meets the specification
  • 0 points — does not meet the specification
• 15 points — for a clear description in your README
  • 15 — thorough discussion of design decisions; a few paragraphs of coherent English sentences should be fine
  • 8 — vague or hard to understand; omits important details
  • 0 — little to no effort, or submitted an RTF/DOC/PDF file instead of plain TXT
• 15 points — for code cleanliness
  • 15 — code is mostly clean and well-commented
  • 8 — code is sloppy and/or poorly commented in places
  • 0 — little to no effort to organize and document code

Note: if your solution is based on pseudo-code from a source other than the textbook or the lecture slides, then you must cite the source of the pseudo-code. Otherwise, you will receive a grade of zero for this assignment.