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 ?

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.

StackExchange Computer Science Q#9484, answer score: 8