6
$\begingroup$

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.

$\endgroup$
0

1 Answer 1

Reset to default
5
$\begingroup$

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.

$\endgroup$
5
  • 1
    $\begingroup$ Thanks for answering. I was looking for either a 3-sat reduction or an algorithm. $\endgroup$
    – yugikaiba
    Dec 28, 2020 at 3:55
  • 1
    $\begingroup$ $x_1$=False, $x_2$=False, $x_3$=False and the formulas are not equisatisfiable. $\endgroup$
    – yugikaiba
    Dec 28, 2020 at 4:35
  • 1
    $\begingroup$ 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. $\endgroup$
    – yugikaiba
    Dec 28, 2020 at 8:01
  • 1
    $\begingroup$ @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. $\endgroup$
    – Anders Kaseorg
    Dec 31, 2020 at 22:16
  • $\begingroup$ true, thank you $\endgroup$
    – yugikaiba
    Jan 1, 2021 at 11:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .