A Resolution Based SAT-solver Operating on Complete Assignments
Eugene Goldberg · Journal on Satisfiability Boolean Modeling and Computation · 2008
Most successful systematic SAT-solvers are descendants of the DPLL procedure and so operate on partial assignments. Using partial assignments is explained by the “enumerative semantics” of the DPLL procedure. Current clause learning SAT-solvers, in a