Search code examples
sat-solverssat

SAT Solvers, 0-depth assignments


When talking about SAT solvers, of the like of minisat for example, what does the value of "0-depth" and "CNF assignments" mean? These values are usually part of the information output of various SAT solvers.


Solution

  • A zero depth assignment is setting a variable's value before DPLL search has begun. The preprocessing of the formula that MiniSAT does (subsumption, self subsumption, etc.) can sometimes prove that a variable must have a certain value. If it can MiniSAT will fix the value of such variables before beginning the DPLL procedure.