Resolution and Clause Learning for Multi-Valued CNF Formulas

ABSTRACT. Conflict-directed clause learning (CDCL) is the basis of SAT solvers with impressive performance on many problems. This performance has led to many reasoning tasks being carried out either by reduction to propositional CNF, or by adaptations of the CDCL algorithm to other logics. CDCL with restarts (CDCL-R) has been shown to have essentially the same reasoning power as unrestricted resolution (formally, they p-Simulate each other). Here, we examine the generalization of resolution and CDCL-R to a family of multi-valued CNF formulas, which are possible reduction targets for a variety of multi-valued or fuzzy logics. In particular, we study the formulas called Signed (or Multi-Valued) CNF formulas, and the variant called Regular Formulas. The main purpose of the paper is to show that an analogous result holds for these cases: a natural generalization of CDCL-R to these logics has essentially the same reasoning power as natural verions of resolution which appear in the literature.