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.

• logic
• propositional-calculus
• np-complete
• satisfiability

1 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) \land (y \oplus x_2 \oplus z) \land (\overline \lor x_3)$$ with $y$ and $z$ as new variables that appear nowhere else in the formula.

$\begingroup$ Thanks for answering. I was looking for either a 3-sat reduction or an algorithm. $\endgroup$

$\begingroup$ $x_1$=False, $x_2$=False, $x_3$=False and the formulas are not equisatisfiable. $\endgroup$

$\begingroup$ the second expression in CNF is equivalent to: $$(\overline \lor \overline \lor z) \land (\overline \lor y \lor \overline) \land (x_1 \lor \overline \lor \overline) \land (x_1 \lor y \lor z) \land (x_2 \lor \overline) \land (x_3 \lor \overline)$$ which is not equisatisfiable with the first. $\endgroup$

$\begingroup$ @yugikaiba For $x_1 = x_2 = x_3 = \textrm$, neither formula is satisfiable: the second reduces to $\overline y ∧ (y ⊕ z) ∧ \overline z$. This answer is correct. $\endgroup$