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: October 28, 2024 (23:45)
• submission of final projects: November 30, 2024

Guidelines

Use your chosen programming language (Pyhon, C#, C++, Java, Haskell, Rust and similar) and the Glucose 4.2 SAT solver. Do not use any other libraries that can convert fomulas to CNF or do similar non-trivial things.

Write a script/program 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 script 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 a README file (plain text, markdown, or pdf) 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, you can check the sample solution of the 15 Puzzle, that was kindly prepared by Dr. Jirka Švancara (thanks!).

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, generalization for an $n\times n$ grid
• Longest Circuit (problem no. 17)
• Maximum Clique
• Maximum Density Still Life
• Minesweeper
• Minimum Test Set (problem no. 44)
• Monochromatic Triangle
• Nonogram
• Numberlink
• Nurikabe, limited to numbers 1 and 2 is fine
• Peaceably Co-existing Armies of Queens, generalization to $n\times n$ chessboard
• 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