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.

• Type: Journal
• Year: 2005
• Where: AMAI
• Authors: Allen Van Gelder
• Keywords: AMAI 2005, Artificial Intelligence, Binary Clauses, Binary-clause Reasoning, Strongly Connected Components