Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

John Slaney, Bruno Woltzenlogel Paleo

This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern SAT-solvers. The resolution inferen…