Schaefer's theorem
From Wikipedia, the free encyclopedia
In computational complexity theory, a branch of computer science, Schaefer's theorem states necessary and sufficient conditions under which a set O of Boolean operators generate polynomial-time or NP-complete problems when some of the operators of O are applied to some of the propositional variables. In particular, it identifies six classes of sets of Boolean operators that generate problems lying in P, while all other classes generate NP-complete problems.
In particular, a set of Boolean operators O, when applied to a set of variables, produces instances that are always polynomial if any one of the following conditions holds for the operators of O:
- all such operators result in true when all its arguments are true;
- all such operators result in true when all its arguments are false;
- all such operators are equivalent to a set of binary clauses;
- all such operators are equivalent to a set of Horn clauses;
- all such operators are equivalent to a set of dual-Horn clauses;
- all such operators are equivalent to a set of affine formulae (e.g., ).
If O is a set of operators satisfying one of these conditions, the problem of establishing the propositional satisfiability of a formula obtained by applying some of these operators to some of the variables lies in P. On the other hand, if a class of such operators does not satisfy any of these conditions, the problem of satisfiability for formulae obtained by applying these operators to some of the variables is NP-complete.
[edit] References
- Schaefer, Thomas J. (1978). "The Complexity of Satisfiability Problems". STOC 1978: 216-226.