Algorithms for computing backbones of propositional formulae.

摘要

The backbone (also called "necessary variables" or "fixed assignments") of a propositional formula <∅ is the set of literals that are true in all models of the formula. Put another way, the backbone is the intersection of all implicants of ∅. Since SAT is NP-complete, deciding if a given literal is in the backbone is co-NP-complete, and computing the backbone is NP-equivalent. Nevertheless, we should no more give up on computing the backbone than we give up on the general SAT problem.