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?
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.
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.
