Labs 03: SAT Solver
In this project, you are given a part of the code for a simple SAT solver in Scala, including its data structure definitions (which are not quite as low level as for a conventional SAT solver). You will need to:
- implement Tseytin's transformation in file Tseytin.scala.
- implement unit propagation using two-watched literals (functions stopWatching, startWatching, propagateClause, and propagate) in file SatSolver.scala.
The backtracking logic is given to you. Do not add additional parts of global solver state, even if this might seemingly improve efficiency, because backtracking code will not support your newly added structures and you do not need to modify the backtracking and decision code for this lab.
Some tests are available in Main to try out your implementation.
This implementation is inspired by the MiniSat paper.