This work introduces the conflict resolution calculus (CR), which is shown to use unification “to generalize conflict-driven clause learning,” and an intermediary calculus, clausal natural deduction (CND). It proves the following:

• Theorem 1: CR simulates resolution
• Theorem 2: refutation is always possible in CR; and
• Theorem 3: CND simulates CR.

With these tools CR is shown to be capable of splitting, and therefore can be written sequentially, thus potentially becoming useful for theorem proving of first-order models. The work is written from a theoretical, albeit practically driven, perspective. Current SAT solvers, such as Equinox, iProver, and AVATAR, are compared with regard to attack variables and implication elimination, where satisfiability is known to be NP-complete. Results suggest that CR might finally lead to “the first-order case through unification.”

The paper does not explore how to implement CR, which would be an important branch of future work.

I strongly recommend this paper to SAT solver researchers and to students willing to read a survey paper about the foundations of SAT solvers and alternative propositions, either using variables or parameters in propositional calculus.