# CNF H is in the class P

CNF H = {<ø>|ø is a satisfiable cnf-formula where each clause contains any number of
literals, but at most one negated literal}


I want to show that CNF H is in P, but I'm having some trouble finding an algorithm. My first idea was to check for each clause c in P if that clause contained at most one negated literal. If no clause contains more than one negated literal, accept, if not, reject.

The problem with this idea is if there is a clause with only one literal, and this literal is negated. Than the clause would be false, and therefore ø is false. How do I write an algorithm that also covers this case?

• The title suggests that you want to show that the problem is NP-complete, but in the text you say "in P", which are you trying? Why is a clause consisting of a single negated literal necessarily false? You can set the variable to false, then the literal evaluates to true (in fact, you have to if the formula is satisfiable). – Luke Mathieson May 21 '14 at 9:42
• Ah, saw the fault now, edited the title. Hm, that's true. But how do I give an algorithm for this? I can't seem to figure out a good method. – user2795095 May 21 '14 at 9:50
• You should be able to find an answer to this yourself, armed with the knowledge that a clause with at most one positive literal is called a Horn clause. (The case with at most one negative literal is equivalent to swapping true and false.) – David Richerby May 21 '14 at 10:58
• Hint: this is HORN-SAT in disguise. Check out en.wikipedia.org/wiki/Horn-satisfiability. – Yuval Filmus May 21 '14 at 13:49
• @user2795095 We're not a homework checking service. You should be able to check your work yourself. If you are unsure about a specific point, you can ask about it. – Yuval Filmus May 21 '14 at 18:02

I have come up with a polynomial-time algorithm for this language that I think is in P.

Possible algorithm (-x means not x).

M = "on input <ø> where ø is a boolean formula in CNF:
1. Repeat until there are no (-x) unit clauses:
For a unit clause (-x), remove all the clauses containing -x from ø
and remove all occurrences of x from the clauses in ø
2. If there is an empty clause in ø, reject.
3. Let all literals x in ø be 1, -x 0, and accept.