A Generalized Framework for Conflict Analysis

This paper makes several contributions to Conflict Driven Clauses Learning (CDCL), which is one of the key components of modern SAT solvers. First, we show that, given an implication graph, asserting clauses derived using the first Unique Implication Point principle (First UIP) are optimal in terms of back-jumping. Secondly we propose an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored by conflict analysis. This extension captures more conveniently the whole propagation process, and opens new perspectives for CDCL-based approaches. Among other benefits, our extension of the implication graph leads to a new conflict analysis scheme that exploits the additional arcs to back-jump to higher levels. Experimental results show that the integration of our generalized conflict analysis scheme within state-of-the-art solvers consistently improves their performance.