# Is Horn-SAT with XOR-relations NP-complete?

I was wondering if the combination of Horn-SAT and XOR-SAT is solvable in polynomial time or not.

It seems they can be solved in polynomial time as both are in class P and also that Horn-SAT is P-complete thus XOR-SAT must be reducible to HORN-SAT .

Just want to clarify if that's the case.

By,HORN-sat with XOR relation I mean a set of clause of the form :

$$(\neg b \lor\neg d \neg c) \land (a \lor \neg b \lor \neg c) \land (b \oplus c \oplus d).$$ Is the set of clause of the form above solvable in polynomial time?

Reductions exist as shown in this question : https://cstheory.stackexchange.com/q/36704/67865 .

But this post shows that its impossible that such a reuction can exist : https://cstheory.stackexchange.com/q/46088/67865.

that;s why i wanted to clarify if they really can be solved in polynomial time and aren't those two post cotradicting each other?

• Please edit your question to define the problem more precisely. It is not clear to me what you mean by the "combination". Please explain how your proposed algorithm would work, and how you'd use the reduction to solve the "combination".
– D.W.
Feb 6 at 5:51
• Please don't use "Edit:", and please don't just append more stuff. Instead, revise the question so it reads well for someone who encounters it for the first time, and presents the problem in a logical order. See cs.meta.stackexchange.com/q/657/755.
– D.W.
Feb 6 at 6:59

Note that we can express variable negation with XOR-clauses, that is, if we have a variable $$x$$, we can introduce a variable $$x'$$ and a XOR-clause $$(x \oplus x')$$, and now $$x' = \lnot x$$. Therefore, we can write arbitrary CNF:s as conjuctions of clauses with only negative literals and XOR-clauses, and therefore Horn-SAT with XOR-clauses is NP-complete.