zbMATH — the first resource for mathematics

Determinization of resolution by an algorithm operating on complete assignments. (English) Zbl 1187.68543
Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 90-95 (2006).
Summary: “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.
For the entire collection see [Zbl 1114.68003].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
BerkMin; Chaff; SATO; UnitWalk
Full Text: DOI