zbMATH — the first resource for mathematics

A decision-making procedure for resolution-based SAT-solvers. (English) Zbl 1138.68539
Kleine B√ľning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 119-132 (2008).
Summary: We describe a new decision-making procedure for resolution-based SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference point under which the number of clauses falsified by the modified point is smaller than for the original one. DMRP makes it possible for a DPLL-like algorithm to perform a “local search strategy”. We describe a SAT-algorithm with conflict clause learning that uses DMRP. Experimental results show that even a straightforward and unoptimized implementation of this algorithm is competitive with SAT-solvers like BerkMin and Minisat on practical formulas. Interestingly, DMRP is beneficial not only for satisfiable but also for unsatisfiable formulas.
For the entire collection see [Zbl 1136.68007].

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