Conditional Pure Literal Graphs

Conditional Pure Literal Graphs (CPLG) characterize the set of models of a propositional formula and are introduced to help understand connections among formulas, models and autarkies. They have been applied to the SAT problem within the framework of refutation- based algorithms. Experimental results and comparisons show that the use of CPLGs is a promising direction towards efficient propositional SAT solvers based upon model elimination. In addition, they open a new perspective on hybrid search/resolution schemes.