0
$\begingroup$
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?

$\endgroup$
  • $\begingroup$ 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). $\endgroup$ – Luke Mathieson May 21 '14 at 9:42
  • $\begingroup$ 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. $\endgroup$ – user2795095 May 21 '14 at 9:50
  • 3
    $\begingroup$ 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.) $\endgroup$ – David Richerby May 21 '14 at 10:58
  • 2
    $\begingroup$ Hint: this is HORN-SAT in disguise. Check out en.wikipedia.org/wiki/Horn-satisfiability. $\endgroup$ – Yuval Filmus May 21 '14 at 13:49
  • 2
    $\begingroup$ @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. $\endgroup$ – Yuval Filmus May 21 '14 at 18:02
1
$\begingroup$

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. 
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.