Optimal Length Tree-Like Resolution Refutations for 2SAT Formulas

摘要

In this article, we exploit the graphical structure of 2SAT formulas to show that the shortest treelike resolution refutation of an unsatisfiable 2SAT formula can be determined in polynomial time.