SAT solver projects

Your task is to create a system that solves a given computational problem using a SAT solver. By default we consider decision problems (answer yes/no), but if it is an optimization problem, consider its decision variant: `Does the given instance have a solution whose objective function has at least/at most a given value?'

Deadlines

• sending preferences for given problems or suggestions for own problems to solve: Oct, 21.
• submission of final projects: Nov, 30.

Guidelines

Use programming language Python 3 and SAT solver Glucose 4.2. Do not use any libraries to convert formulas into CNF or something nontrivial.

Write a script that:

• takes an instance of the problem on input (given by some parameters or by a path to file with the instance, or both),
• encodes the instance into SAT problem in the DIMACS CNF format,
• calls the SAT solver Glucose on this CNF formula,
• decodes the solution of SAT (if it exists) back to the solution of the problem,
• outputs the solution in some humanly readable format.
• The skript should also have an option to output the constructed CNF formula in DIMACS format, and statistics about the solution reported from the SAT solver.

In your submission, apart from the script you should include several instances, in particular:

• a small positive (satisfiable) humanly readable instance,
• a small negative (unsatisfiable) humanly readable instance (if it exists),
• a nontrivial satisfiable instance that runs at least 10s (and max 10 mins), if you cannot find it, describe what you tried.

Your submission must include README.md file with a brief documentation explaining:

• an exact description of the problem that you solve (parameters, constraints, etc.)
• a description of your encoding into CNF including meaning of your propositional variables, and discussion of possible alternatives
• a user documentation to your script (input format and output format if not obvious)
• a description of attached instances
• a report on experiments that you have done (how large instances your script can solve in a reasonable time)

Ethical rules

You have to work completely independently without any external help other than the teacher. You can search for additional information about the given problem (e.g. interesting instances or if you are not clear about the specification of the problem), but it must not refer to its encoding into CNF or using the SAT solver to solve it. You must also not read any code solving the given (or related) problem. In case of confusion how to proceed, contact me and I will provide you with assistance or help.

Sample solution

For inspiration please check a sample solution of the problem 15 Puzzle, which was kindly prepared by dr. Jiri Svancara (thank you!).

Problem selection

Each student in the same class will solve a different problem. You can choose a problem from the list below or you can submit your own suggestions for a different problem that you are interested in. In this case, describe the problem and why you choose it. It must be approved first as it should be reasonably difficult (so please also include your preferences for the problems from the list).

Send me your preferences by email by the deadline above. You should include at least 10 problems (no upper bound) of your choice, each on separate line in the order of your preference. In case of conflict in your first preference with other students, I will assign the problem to a random student, and then proceed further in the list. In case you do not send me your preferences by the deadline, you will be assigned a random problem that is left.

Submissions

Final project can be submitted as a link to a public GitHub or GitLab repository, or in .zip file.

List of problems

• Bipartite Dimension
• Clique Cover
• Cubic Subgraph (problem no. 26)
• Degree-constrained Spanning Tree
• Domatic Number
• Exact Cover
• Graph Isomorphism
• Graph Partitioning (problem no. 25)
• Hamiltonian Path
• Induced Subgraph Isomorphism
• Intersection Number
• Kernel (problem no. 18)
• Killer Sudoku, a generalisation for the grid n x n (where n is a square)
• Longest Circuit (problem no. 17)
• Maximum Clique
• Maximum Density Still Life
• Minesweeper
• Minimum Test Set (problem no. 44)
• Monochromatic Triangle
• Nonogram
• Numberlink
• Nurikabe, restricted to numbers 1 and 2
• Peaceably Co-existing Armies of Queens, a generalisation for the chessboard n x n
• Rural Postman (problem no. 34)
• Set Cover
• Set Packing
• Set Splitting
• Shortest Common Superstring (problem no. 16)
• Slitherink
• Social Golfers Problem
• Sports Tournament Scheduling
• Square-Tiling (problem no. 54)
• Steiner Triple Systems
• Subgraph Isomorphism
• Three-dimensional Matching
• Word Design for DNA Computing on Surfaces