[Solved]: 3-SAT where variables occur equally many times as a positive literal and as a negative literal

Problem Detail: 

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?

Asked By : Juho

Answered By : Xavier Labouze

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.

Best Answer from StackOverflow

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