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

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.

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.
• $x_1$=False, $x_2$=False, $x_3$=False and the formulas are not equisatisfiable. Dec 28, 2020 at 4:35
• the second expression in CNF is equivalent to: $$(\overline{x_1} \lor \overline{y} \lor z) \land (\overline{x_1} \lor y \lor \overline{z}) \land (x_1 \lor \overline{y} \lor \overline{z}) \land (x_1 \lor y \lor z) \land (x_2 \lor \overline{y}) \land (x_3 \lor \overline{z})$$ which is not equisatisfiable with the first. Dec 28, 2020 at 8:01
• @yugikaiba For $x_1 = x_2 = x_3 = \textrm{False}$, neither formula is satisfiable: the second reduces to $\overline y ∧ (y ⊕ z) ∧ \overline z$. This answer is correct. Dec 31, 2020 at 22:16