Concurrent CDCL SAT-Solver

  • Source: Software project as part of Modern Imperative Programming Languages Seminar
  • Type: Group student project (of 3 students)
  • Language(s): Rust
  • Description:

As part of a student group, I planned and implemented a concurrent Conflict-Driven Clause Learning SAT-Solver using the modern imperative programming language Rust. We optimised literal assignment using multiple heuristic strategies, detected and handled pure variables for efficiency and parallelised the solver’s processing.