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
