S-SAT - Sapienza SAT
Introduction | Documentation | Download | Contact


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.

Copyright (c) Donato Capitella