On Conflict-Driven Reasoning

Automated formal methods and automated reasoning are interconnected, as formal methods generate reasoning problems and incorporate reasoning techniques. For example, formal methods tools employ reasoning engines to find solutions of sets of constraints, or proofs of conjectures. From a reasoning perspective, the expressivity of the logical lan- guage is often directly proportional to the difficulty of the problem. In propositional logic, Conflict-Driven Clause Learning (CDCL) is one of the key features of state-of-the-art sat- isfiability solvers. The idea is to restrict inferences to those needed to explain conflicts, and use conflicts to prune a backtracking search. A current research direction in auto- mated reasoning is to generalize this notion of conflict-driven satisfiability to a paradigm of conflict-driven reasoning in first-order theories for satisfiability modulo theories and as- signments, and even in full first-order logic for generic automated theorem proving. While this is a promising and exciting lead, it also poses formidable challenges.