The goal of the project is to implement your own simple CDCL-based SAT solver. You can work in pairs, but you do not have to.

The only hard requirement is the list of techniques that your solver has to implement (see below). There are no minimal requirements on the performance of the solver. However, I will be periodically running your solvers on a set of benchmarks and you will see a table that compares performance of your solver to the solvers submitted by your fellow students.

Functionality

There is minimal functionality required of your solver. Your solver must implement:

• input in DIMACS format;
• output according to rules of SAT competition, i.e, each line of the output is either a comment line (c TEXT), model value line (v LITERALS), or a solution line (s RESULT), where RESULT is either SATISFIABLE, UNSATISFIABLE or UNKNOWN);
• Boolean constraint propagation using two-watched-literals scheme;
• conflict-driven clause learning (you can experiment with multiple learning algorithm, but first unique implication point (UIP) is completely sufficient);
• a nontrivial decision variable heuristic (such as VSIDS, but feel free to experiment with others);
• restarts (you can experiment with multiple restart schemes);
• models generation for satisfiable formulas in the format of SAT competition, i.e., a line v LITERALS 0, where LITERALS is a sequence of non-contradictory literals (positive numbers for positive polarity, negative for negative polarity) such that at least one literal of each clause is in the sequence LITERALS. For example v 1 -2 0 is an assignment that assigns variable 1 to true and variable 2 to false.

However, there is no limit on what your solver can implement. If you read up on any more advanced functionalities and implement them, it will be an advantage during your oral exam. Some suggestions:

• phase saving and rephasing,
• learnt clause forgetting based on activity heuristic,
• learnt clause minimization,
• preprocessing and inprocessing (pure literal elimination, removal of subsumed clauses, blocked clause elimination, …), beware that if you implement any preprocessing or inprocessing, you have to modify model generation as well: you have to produce a model of the original formula, not the preprocessed one,
  
• proof generation for unsatisfiable formulas (preferrably in DRUP or DRAT format),
• solving under assumptions (see Minisat),
• generation of unsatisfiability cores or failed assumption literals,
• clause vivification.

Implementation

You can use any reasonable programming language, e.g. C, C++, C#, F#, Go, Java, Kotlin, Python, Scala, OCaml, Rust, etc. Your solver should be usable on Ubuntu 22.04 without any complicated setup.

Please, only use standard libraries that come with your language. If you have any extra requirements (e.g., NumPy), write me an email and we can discuss those.

For testing, choose some benchmarks from SAT-LIB repository. Testing on Uniform Random-3-SAT benchmarks should be sufficient.

If you can read C++, you can check out MiniSAT (recommended) or CaDiCaL (advanced) to see how some of the techniques can be implemented. If you copy any ideas or (especially!) parts of code, mention this in the comments.

Deadlines

There are three basic milestones that you have to meet.

Week 3: Create a repository

By the end of third week of the semester (March 10), create a repository for your SAT solver on the faculty GitLab. Write a simple README that contains the names of the team members (one or two students) and the name of your SAT solver.

Grant me an access to your repository and send me and email with a link to your repository.

Week 6: Create an executable

By the end of sixth week of the semester (March 31), create an executable/main script for your SAT solver. Extend the README with instructions of how to compile and execute the solver. At this point, it is ok if the solver always responds s UNKNOWN, but you are encouraged to already implement some parts of the solver.

If your SAT solver requires compilation or more complicated setup, please use a standard build tool (CMake, cargo, …). Ideally, provide a simple Makefile that I can use to compile your solver and also document its usage in the README. If the setup is even more complicated, you can also provide a Dockerfile that I can run to create an image for a container with the solver.

(The main purpose of this step is that I can check whether your solver works on my machines and that I can set up the testing environment that will automatically run your solver on the set of benchmarks.)

End of semester (May 19): Finish the solver

Complete the solver. Extend the README with the description of what your solver implements and why. If you have any interesting observations, I will be happy to read those as well.