vw-passat

A simple CDCL-based SAT solver developed within the course IA085 Satisfiability and Automated Reasoning at FI MUNI.

Author: Jakub Janků (514496)

How to get it moving

First, compile the project:

cargo build --release

The output binary is stored in target/release/vw-passat. Your Passat is now ready to go!

Basic usage:

vw-passat input.cnf

The solution is printed to stdout.

For more advanced options, see vw-passat --help

Implemented functionality

Required:

• Input in DIMACS format (io)
• Output in SAT Competition format (io)
• Unit propagation using two watched literals (solver)
• Conflict-driven clause learning (CDCL) (solver)
• EVSIDS branching heuristic (activity)
• Restarts using Luby sequence (restart)

Additional:

• Parallelization (parallel)
• Phase saving (assignment)
• Clause forgetting (activity, solver)
• Basic learnt clause minimization (solver)
• DRAT proof generation (plain, binary) (drat)
• Simple benchmarking utility & analysis script (benchmark, analysis)

Remarks

• Parallelization was an easy way to increase performance of the solver significantly (~100 LOC, see parallel). Resource utilization could be improved further by assigning new work to threads that finish early.
• Forgetting was implemented mainly to reduce the number of cache misses. This effort seems to have paid off. Additionally, it opens new possibilities for optimization because it changes the hot path (previously, up to 90 % of the execution time was spent in unit propagation, this is now reduced to 50 % or less).
  • However, at the current state of the project, it largely means that bad code can no longer be excused with "this runs 1 % of the overall time" :/ For example, conflict analysis relies on sorting to deduplicate literals in clauses, the heap implementation performs unnecessary writes, etc. These suboptimalities seem to be no longer so insignificant.
• Proof checker, drat-trim specifically, is used in tests to reduce the probability of any subtle bugs hiding in the solver (see integration and CI setup). Proofs are generated for both UNSAT as well as SAT instances.
• Low "restart sequence multiplier" (the number by which the Luby sequence is scaled) seems to hurt the performance on large instances despite the paper linked in the interactive syllabus, Evaluating CDCL Restart Schemes, suggesting otherwise. (But there is a chance that I misunderstood it, I just skimmed through it.)
• Remaining features were implemented for obvious reasons.