# Is NAE-HORN-SAT in P or NP-hard?

I am interested to know the complexity of the NAE-HORN-SAT problem (not all equal). We know that HORNSAT is $\mathsf{P}$-complete, but on the other hand, NAE-SAT is $\mathsf{NP}$-complete. I want to know what can we say about NAE-HORN-SAT problem. Let me define the problem formally:

Given: One Boolean formula $\phi$ is given to us in CNF where each clause has at most one positive literal (HORN-property).
Question: Is there any assignment for the input variables of $\phi$ such that any clause has at least one False and at least one True literal (NAE-property) ?

N.B.:

• Positive literal: any variable directly,
• Negative literal: negation of any variable.
• True literal: literal is assigned to Boolean True by any assignment,
• False literal: literal is assigned to Boolean False by any assignment.

According to Schaefer's dichotomy theorem, this problem must be either in $\mathsf{P}$ or $\mathsf{NP}$-complete. I can just find one polynomial reduction from HORNSAT to this problem, which proves actually nothing. Is there a polynomial time algorithm to solve this problem?

Or, is there any way to prove this problem to be $\mathsf{NP}$-hard? Any thoughts about this ?

• Schaefer’s theorem does not just tell that the problems of this kind (namely, Boolean k-CSPs with a fixed k and a fixed set of k-relations) are either in P or NP-complete. It characterizes exactly which of these problems are in P and which are NP-complete. Try harder to use Schaefer’s theorem, and you will obtain the answer. Feb 4, 2013 at 16:20

Your problem, NAE-HORN-SAT is $NP$-complete. Monotone NAE-SAT is $NP$-complete and it is a special case of your NAE-HORN-SAT. Literals in monotone SAT formula are either all positive or all negative.
Schaefer's dichotomy theorem actually doesn't necessarily apply in this case, since the width of clauses in a NAE-HORN-SAT formula isn't bounded. What Schaefer's theorem does give you is an algorithm which decides, for each $k$, whether the restriction of NAE-HORN-SAT to clauses of width $k$ (or up to $k$) is in P or NP-complete. The algorithm appears in the Wikipedia page, and you can look up some of the references (e.g. the recent survey by Chen) for more explanations.
In your case, there are two possibilities. The first possibility is that for some $k$, NAE-HORN-SAT is NP-complete for clauses of width $k$. The second possibility is that for all $k$, NAE-HORN-SAT is in P. In the latter case, you will have to look at the algorithm which solves NAE-HORN-SAT for each bounded $k$ (there is an algorithm for each of the six easy cases listed in the theorem, and you will end up with one of them), and check whether it generalizes to unbounded width. If it doesn't, then come back to us and ask the question again. Edit: we don't expect this to happen, see this question.