Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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) ?


  • 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 ?

share|cite|improve this question

migrated from Feb 4 '13 at 19:13

This question came from our site for theoretical computer scientists and researchers in related fields.

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. – Tsuyoshi Ito Feb 4 '13 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.

Take any instance of Monotone NAE-SAT problem (all its literals are negative) then this formula is an instance of NAE-HORN-SAT problem.

share|cite|improve this answer

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.

Note that if the clause width is unbounded, then the general CSP problem isn't guaranteed to be in NP (or even computable), though in your case it is.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.