In the paper The complexity of satisfiability problems MR0521057, Tom Schaefer characterizes exactly which general classes of satisfiability problems are in P and which are NP-complete. Those problems which are in P fall into six cases:
Every relation in S is satisfied when all variables are 0.
Every relation in S is satisfied when all variables are 1.
Every relation in S is definable by a CNF formula in which each conjunct has at most one negated variable.
Every relation in S is definable by a CNF formula in which each conjunct has at most one unnegated variable.
Every relation in S is definable by a CNF formula having at most 2 literals in each conjunct.
Every relation in S is the set of solutions of a system of linear equation over the two-element field {0,1}.
Here, S is a set of boolean relations that one takes as primitives for the language; the associated satisfiability problem is then deciding the satisfiability of a finite conjunction of such primitives. Schaefer moreover shows that any set of relations which does not fall into one of the above has a NP-complete satisfiability problem. In your example, S would be a set of boolean relations definable by a CNF formulas in which each conjunct has at most two unnegated variables. This is not in the above list, so the corresponding satisfiability problem is NP-complete.
No comments:
Post a Comment