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?