# Complexity of deciding the satisfiability of a quasi-monotone CNF formula

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?

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.