[Solved]: Complexity of deciding the satisfiability of a quasi-monotone CNF formula

Problem Detail: 

A quasi-monotone CNF formula is a formula where each variable appears at most once as a positive literal (and any number of times as a negative literal).

What is the complexity of deciding its satisfiability?

Asked By : Xavier Labouze

Answered By : Realz Slaw

Obviously this can be solved with the same complexity as boolean SAT. The question is, can we do better. The answer is no: this problem is NP-complete.

You can show it is NP-complete by reducing a regular CNF formula to "quasi-monotone" CNF, as follows:

Since you cannot use positive terms in general, what you want is a new, equivalent, variable in-place of the positive terms. So let $\Phi = {\LARGE\bigwedge}C_i$ be a general boolean sat formula. We will replace all non-negated $x_j$ terms with new variables called $\neg n_{x_j}$. Then, we need to constrain $n_{x_j} = \neg x_j$; so we introduce the following clauses:

$$\left(n_{x_j} \implies \neg x_j\right) \wedge \left(\neg x_j \implies n_{x_j}\right)$$

This essentially means that $n_{x_j} = \neg x_j$. Written in CNF:

$$\left(\neg n_{x_j} \vee \neg x_j\right) \wedge \left(x_j \vee n_{x_j}\right)$$

These two clauses will effectively allow you to replace all your other non-negated terms, and they only leave behind a single non-negated term for each literal (within these clauses), which is allowed in "quasi-monotone" CNF as defined by the question.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/16483

3.2K people like this

 Download Related Notes/Documents