1
$\begingroup$

Definitions:

positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula.

negative CNF is a conjunctive normal form formula, where all literals are negative, i.e. the unary connective ¬ appears next to each literal.

My question is:

Given a CNF, which is a conjunction of positive CNF and negative CNF, what is the complexity of the problem to determine that this special case of CNF is satisfiable?

Does exist polynomial time and space algorithm to solve this problem?

EDIT: Another name for "positive CNF" is "fact CNF", where all clauses are fact and another name for "negative CNF" is "goal CNF", where all clauses are goal.

... clause with no negative literals is sometimes called a fact
... clause without a positive literal is sometimes called a goal clause

Quoted from: this wikipedia documentation

Improve this question
$\endgroup$
4
  • $\begingroup$ npcomplete.owu.edu/2014/07/22/not-all-equal-3sat ​ ​ $\endgroup$
    – user12859
    Commented Jul 22, 2017 at 23:38
  • $\begingroup$ Nice article, but the problem in this question isn't NAE3SAT, unless it can be reduced to NAE3SAT. If it can be reduced to NAE3SAT, then can you show this as answer to my question please? $\endgroup$
    – Farewell Stack Exchange
    Commented Jul 23, 2017 at 0:36
  • $\begingroup$ Monotone NAE constraints are conjunctions of positive clauses and negative clauses. ​ ​ $\endgroup$
    – user12859
    Commented Jul 23, 2017 at 0:37
  • $\begingroup$ Where positive clause is fact and negative clause is goal? $\endgroup$
    – Farewell Stack Exchange
    Commented Jul 23, 2017 at 0:38

1 Answer 1

Reset to default
4
$\begingroup$

Given a CNF, which is a conjunction of positive CNF and negative CNF, what is the complexity of the problem to determine that this special case of CNF is satisfiable?

The problem is provably NP-complete by reduction from CNF satisfiability.

Each negative literal $\lnot{x}$ in a CNF SAT instance can be converted to a positive literal by replacing all occurrences of it with a new variable $z$ plus the following two CNF clauses: $x \lor z$ and $\lnot{x} \lor \lnot{z}$. The clauses force $z$ to act as the same constraint as $\lnot{x}$. Once all the original negated literals have been replaced, you are left with clauses that contain either all positive or all negative literals. Since any CNF SAT instance can be reduced to this form and since CNF SAT is NP-complete and since your problem is trivially in NP, your problem must be NP-complete.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Excellent and correct answer to my question. $\endgroup$
    – Farewell Stack Exchange
    Commented Jul 23, 2017 at 2:26
  • $\begingroup$ And if each positive/fact clause has at most 2 positive literals? $\endgroup$
    – Farewell Stack Exchange
    Commented Jul 23, 2017 at 10:28
  • 1
    $\begingroup$ @ErezZrihen, that's a new question, which should be asked separately -- but first you should spend some time trying to figure it out. It looks like a straightforward modification of this reduction should work. $\endgroup$
    – D.W. ♦
    Commented Jul 23, 2017 at 16:22
  • $\begingroup$ I will ask new question then. $\endgroup$
    – Farewell Stack Exchange
    Commented Jul 23, 2017 at 16:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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