Consider the following 3-SAT variant defined over the variables $x_1,\ldots,x_n$. In the $k$P$k$N-3SAT problem each variable $x_j$, $j \in [n]$, occurs exactly $k$ times as a positive literal in $\phi$, and exactly $k$ times as a negative literal in $\phi$, where $\phi$ is a 3-CNF formula. The problem is then to decide if such a formula has a satisfying assignment.

Is the $k$P$k$N-3SAT problem NP-complete?

In the $m$P$n$N-SAT problem each positive literal occurs exactly $m$ times in $\phi$, and each negative literal occurs exactly $m$ times in $\phi$, where $\phi$ is a CNF formula. It was shown in [1] that $2$P$1$N-SAT is NP-complete. This hints that the $k$P$k$N-3SAT problem is hard as well.

The $1$P$1$N-SAT is apparently easy, see a related question and answer here. Is $k$P$k$N-3SAT perhaps hard already for $k \geq 2$?

[1] Yoshinaka, Ryo. "Higher-order matching in the linear lambda calculus in the absence of constants is NP-complete." Term Rewriting and Applications. Springer Berlin Heidelberg, 2005. 235-249.


2 Answers 2


1) 2P2N-3SAT is NP-complete

(Edit to take into account all comments below)

Take a 2P1N-SAT instance, check the all-1 vector is not a model, then add the clause with all variables negated to the formula to transform it into a 2P2N-SAT instance.

For each 1-clause $(a)$ in the new 2P2N formula, replace it by the three following 3-clauses : $(a \lor x \lor x)(\lnot x \lor y \lor y)(\lnot x \lor \lnot y \lor \lnot y)$ where $x,y$ are fresh 2P2N variables (i.e. appearing twice as positive literals and twice as negative literals).
For each 2-clause $(a \lor b)$ in the formula, replace it by the six following 3-clauses : $(a \lor b \lor x)(\lnot x \lor y \lor y)(\lnot x \lor \lnot y \lor \lnot y)(x \lor z \lor \lnot z)(z \lor t \lor \lnot t)(\lnot z \lor t \lor \lnot t)$ where $x,y,z,t$ are fresh 2P2N variables.
Keep all 3-clauses in the formula.
For each $k$-clause ($k>3$) in the formula, transform it into a set of 3-clauses by the usual way, which does not change the number of occurences of positive (negative) literals of the taken $k$-clause, but add only extra variables which appear once as a positive literal and once as a negative literal. For each such new variable $x$, add the two following clauses to the 3-CNF formula : $(x\lor y \lor \lnot y)$ and $(\lnot x \lor \ y\lor \lnot y)$ where $y$ is a fresh 2P2N variable.

All these transformations can obviously be done in polynomial time and transform the 2P1N-SAT instance into a 2P2N-3SAT instance. The NP-complete 2P1N-SAT problem is then reducible to the 2P2N-3SAT problem.

2) The extension to $k$P$k$N-3SAT can be done in the same spirit (a bit longer) to prove it is NP-complete as well.


As confirmed independently in another answer, 2P2N-3SAT is already NP-complete. Another name for the fragment you are interested in is (3, B$k$)-SAT where "B" stands for Balanced and indicates that there are the same number of positive and negative occurences of the variables, $k$ is the number of positive and the number of negative occurences, and the 3 indicates the size of clauses: we are indeed in a fragment of 3SAT.

In particular, 2P2N-3SAT is the same as (3, B2)-SAT and this fragment was proven NP-complete as Theorem 1 in [1].

A related natural question is: given that 2P2N-3SAT is NP-complete, and given that 2P1N-SAT is NP-complete, what about about 2P1N-3SAT? This one turns out to be trivial: all instances are always satisfiable, Theorem 2.4 in [2]. If you allow some clauses to have fewer than 3 variables, then the satisfiability problem is NP-complete as observed in Theorem 2.1 in [2].

[1] Piotr Berman, Marek Karpinski, Alexander D. Scott. Approximation hardness of short symmetric instances of MAX-3SAT, Electronic Colloquium on Computational Complexity, Technical Report TR03-049 (2003)
[2] Tovey, Craig A. A simplified NP-complete satisfiability problem, Discrete applied mathematics 8.1 (1984): 85-89.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.