Documentation
Here I'll basically provide documentation about the Boolean Satisfability problem and the structure of S-SAT.
S-SAT development was divided into three modules:
- DIMACS Parser:
This module implements a parser able to read DIMACS file and cnf formulas.
- Unit Propagation:
This module implements the unit propagation which is the mean through
which S-SAT is able to understand if an aissignment brings to conflic,
forces other assignmets or satisfies a given formula.
- Backtracking System:
If we stumble into a conflic we need to take some step backs, undo the assignments that caused the conflict and try other paths.
|