3-SAT where variables occur equally many times as a positive literal and as a negative literal

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?

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.

StackExchange Computer Science Q#16672, answer score: 11