You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

A Resolution Based SAT-solver Operating on Complete Assignments


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 sense, have outgrown this semantics. Instead of enumerating the search space as the DPLL procedure does, they explicitly build a resolution proof. In this paper, we suggest a semantics that, in our opinion, is more suitable for clause learning SAT-solvers. The idea is to consider a set of complete assignments not just as a part of the search space but as an “encryption” of a resolution proof or a part thereof. Importantly, a set of points encrypting a resolution proof can be dramatically smaller than the entire search space. We introduce a resolution based SAT-solver with clause learning called FI (short for Find point Image of a proof) that is inspired by the new semantics. FI operates on complete assignments. We compare our naive implementation of FI with Minisat and BerkMin. Experiments show that FI is competitive with Minisat and BerkMin in terms of backtracks. In terms of performance, FI is slower than Minisat and BerkMin for small CNF formulas. On the other hand, even the current primitive implementation of FI is competitive with Minisat and BerkMin on large Bounded Model Checking formulas due to its superior decision making.