Sciweavers

AMAI
2005
Springer

Toward leaner binary-clause reasoning in a satisfiability solver

13 years 11 months ago
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.
Allen Van Gelder
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where AMAI
Authors Allen Van Gelder
Comments (0)