The Not All Equal $k$-SAT problem (NAE $k$-SAT), given a set $C$ of clauses over a set $X$ of boolean variables such that each clause contains at most $k$ literals, asks whether there exists a truth assignment of the variables such that each clause contains at least one true and at least one false literal.

The PLANAR NAE $k$-SAT problem is the restriction of NAE $k$-SAT to those instances where the incidence bipartite graph of $C$ and $X$ (i.e. the graph of parts $C$ and $X$ with an edge between $x\in X$ and $c\in C$ if and only if $x$ or $\overline{x}$ belongs to $c$), is planar.

It is known that NAE 3-SAT is NP-complete (Garey and Johnson, Computers and Intractability; A Guide to the Theory of NP-Completeness), but PLANAR NAE 3-SAT is in P (see Planar NAE3SAT is in P, B. Moret, ACM SIGACT News, Volume 19 Issue 2, Summer 1988 - unfortunately I do not have access to this paper).

Is PLANAR NAE $k$-SAT in P for some $k\geq 4$? Is there a value of $k$ for which it has been shown to be NP-complete?


1 Answer 1


PLANAR NAE $k$-SAT is in P for all values of $k$ .

Reason is that we can reduce PLANAR NAE $k$-SAT to PLANAR NAE $3$-SAT. Let $\phi$ be an instance of PLANAR NAE $k$-SAT, and suppose $\phi$ contains a clause $C$ with literals $\ell_1, \ell_2, \dots, \ell_k$. Introduce a new variable $v_C$, and replace $C$ with two NAE clauses $C_1$ and $C_2$. $C_1$ contains $3$ literals $\ell_1$, $\ell_2$, and $v_C$, while $C_2$ contains $k-1$ literals $\bar{v}_C, \ell_3, \ell_4, \dots, \ell_k$. It's easy to see that $C$ is satisfiable iff $C_1 \wedge C_2$ is and that the transformation preserves planarity. Now, we can repeatedly apply this procedure on the clauses to eventually obtain an instance $\phi'$ of NAE $3$-SAT as desired.

  • 1
    $\begingroup$ Great answer. Was this already known? $\endgroup$ Commented Apr 11, 2011 at 15:40
  • 1
    $\begingroup$ It sounds like this reduction "works" even without the planar proviso, so it's probably "known" $\endgroup$ Commented Apr 11, 2011 at 16:07
  • $\begingroup$ @Serge I'm sure it was, but I don't know of a reference. $\endgroup$
    – arnab
    Commented Apr 11, 2011 at 16:07
  • 6
    $\begingroup$ It is a standard reduction, which also works for "regular" SAT. You can find it e.g. in Sipser's book "Introduction to the Theory of Computation" and in many more. $\endgroup$
    – 5501
    Commented Apr 11, 2011 at 18:51

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.