Is XOR-SAT + $2$-SAT in P?

Question

I read in a paper a proof where you can reduce a $3$-SAT problem into $2$-SAT + HORN-SAT clauses.

$2$-SAT + HORN-SAT is therefore, NP-complete.

$2$-SAT, HORN-SAT, DUAL HORN-SAT, XOR-SAT are all in P.

I would like to know, if there is a Polynomial time algorithm for the conjuntion of $2$-SAT and XOR-SAT formulas.

Answer 1

There is no polynomial-time procedure for deciding the satisfiability of 2-SAT + XOR-SAT unless P = NP. So, probably not. 2-SAT + XOR-SAT is easily proven NP-complete by direct polynomial reduction from 3-SAT.

In a 3-SAT instance, each 3-CNF clause $$(x_1 \lor x_2 \lor x_3)$$ can be rewritten into the equisatisfiable 2-SAT + XOR-SAT expression $$(x_1 \lor \overline{y}) \land (y \oplus x_2 \oplus z) \land (\overline{z} \lor x_3)$$ with $y$ and $z$ as new variables that appear nowhere else in the formula.