Let $\phi$ be a 3-CNF formula over variables $x_1,x_2,\ldots,x_n$. Every variable $x_i$, $i \in [n]$, occurs equally many times as a positive literal and as a negative literal in $\phi$.

Is it NP-complete to decide the satisfiability of such a formula? Assuming it is, I would be interested in knowing if it has a special name. Has it perhaps also been investigated somewhere?

| cite | improve this question | | | | |

The problem has been studied as $m$P$n$N-SAT problem by Ryo Yoshinaka in Higher-Order Matching in the Linear Lambda Calculus (in 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings).

The $m$P$n$N-SAT is a SAT problem where each positive literal occurs exactly $m$ times and each negative literal exactly $n$ times. It has been shown that even $2$P$1$N-SAT is NP-complete. Note that $1$P$1$N-SAT is in P since each variable can easily be removed after a single step of resolution, which doesn't increase the number of clauses in the formula.

| cite | improve this answer | | | | |

It is NP-complete (but I don't know if it has a name): suppose that a variable $x_i$ appears as a positive literal $n$ more times than as a negative literal.

Then you can "balance" it adding $n$ new 3CNF clauses with $n$ new variables $y_1,...,y_n$:

$-x_i \lor y_1 \lor -y_2$
$-x_i \lor y_2 \lor -y_3$
$-x_i \lor y_{n-1} \lor -y_n$
$-x_i \lor y_n \lor -y_1$

If $x_i$ appears more times as a negative literal, apply the same expansion but using $x_i$ in the new 3CNF clauses instead of $-x_i$.

The $y_i$ are balanced and the resulting formula (that can be built in polynomial time) is clearly satisfiable if and only if the original 3CNF formula is satisfiable: whatever is the value of $x_i$ the new clauses can be satisfied setting $y_i = true$, so they don't "interfere" with the satisfiability of the original formula.

| cite | improve this answer | | | | |

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.