The Complexity of Pure Literal Elimination

摘要

The computational complexity of eliminating pure literals is calibrated for various classes of CNF formulas. The problem is shown to be P-complete in general, NL-complete for 2-CNF, and SL-complete for CNF formulas with at most two occurrences of each variable.