A.: Toward leaner binary-clause reasoning in a satisfiability solver

Binary-clause reasoning has been shown to reduce the size of the search space on many satisfiability problems, but has often been so expensive that run-time was higher than that of a simpler procedure that explored a larger space. The method of Sharir for detecting strongly connected components in a directed graph can be adapted to performing “lean ” resolution on a set of binary clauses. Beyond simply detecting unsatisfiability, the goal is to find implied equivalent literals, implied unit clauses, and implied binary clauses.