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 ?