Programming tasks

Note that the list is not necessarily complete and further tasks may be added throughout the semester.

General notes

• There are no deadlines for the tasks listed below
• The choice of programming language is up to you, as far as your program can be compiled and run on a Linux
• Write readable code
• The number of points for each task is an upper bound, the actual number of points is determined based on the quality of your solution. If a report is required, then the quality of the report is included into the evaluation as well.
• If you use the faculty GitLab server or another similar service (GitHub etc.), you can just point me to the source code in this way. It might be easier than sharing the code via e-mail.

Build your own SAT solver and related tasks

In this set of tasks the ultimate goal is to have a solver at the end (for checking SAT, maybe extended with model counting). The development of the solver is split into several steps each of which is given as a separate task. That said, each tasks assumes you have already finished the preceding tasks (or some of them) and you can build on them. Bear that in mind during programming (i.e. you should write code which can be easily reused for the next tasks). Also, note that given the nature of the tasks a single program can be submitted as a solution to several tasks, it is your choice what you want to implement.

1. Tseitin Encoding and DIMACS Format [5 points]
2. DPLL Algorithm [5 points]
3. Watched Literals [5 points]
4. CDCL [10 points]
5. Decision Heuristics [5 points]
6. Look-Ahead Solver [10 points]

Using a SAT solver

For solving these tasks, you can use a SAT solver or programming language of your choice. For the solvers I can recommend

• Your CDCL or Look-Ahead solver (best choice of course, if you have one)
• MiniSat
• Glucose
• Lingeling
• CaDiCal
• Sat4j
• PySAT — not a solver, but a python toolkit for using a SAT solver as an oracle

Particular choice is not too important, I personally use Glucose for most purposes, MiniSat is still very good as well. CaDiCal won the SAT competition in year 2019 so it looks like a good choice as well. Sat4j is particularly useful if you want to use Java.

Most of the solvers can be compiled as a library which can be linked with your program, they are usually written in C++. If you want to use Java, then I would consider using Sat4j. If you want to use Python, then you can use PySAT toolkit.

For some of the tasks you can also use an SMT solver (e.g. N Queens Puzzle or Cryptarimethics). I can recommend.

• Z3 by Microsoft
• CVC5 which is open source

You can also consider

• Yices2
• Boolector (this one can work only with theories of fixed-size bit-vectors, arrays and uninterpreted functions)

Note that the SMT solvers are usually able to read SMT-LIB format version 2, so if you consider it as an intermediary format, you can use any SMT solver. Most of the solvers usually offer a good API for C++ or Python (at least Z3 and CVC5) do).

List of tasks

• N Queens Puzzle [5 points]
• Cryptarimethics [5 points]
• Nonogram solver[5 points]
• Backbones [5 points]
• Testing equivalence [5 points]
• Making a CNF prime and irredundant [5 points]

If you have any good idea for an application of a SAT/SMT solver, then let me know and I can make it a task as well.