Determinization of Resolution by an Algorithm Operating on Complete Assignments

摘要

"Determinization" of resolution is usually done by a DPLL-like procedure that operates on partial assignments. We introduce a resolution-based SAT-solver operating on complete assignments and give a theoretical justification for determinizing resolution this way. This justification is based on the notion of a point image of resolution proof. We give experimental results confirming the viability of our approach. The complete version of this paper is given in [2].