13
$\begingroup$

I'm wondering if there is a polynomial algorithm for "2-SAT with XOR-relations". Both 2-SAT and XOR-SAT are in P, but is its combination?

Example Input:

  • 2-SAT part: (a or !b) and (b or c) and (b or d)

  • XOR part : (a xor b xor c xor 1) and (b xor c xor d)

In other words, the input is the following boolean formula:

$$(a \lor \neg b) \land (b \lor c) \land (b \lor d) \land (a \oplus b \oplus \neg c) \land (b \oplus c \oplus d).$$

Example Output: Satisfiable: a=1, b=1, c=0, d=0.

Both the number of 2-SAT clauses and the number of XOR clauses in the input are $O(n)$, where $n$ is the number of boolean variables.

Improve this question
$\endgroup$
1

3 Answers 3

Reset to default
12
$\begingroup$

2-SAT-with-XOR-relations can be proven NP-complete by reduction from 3-SAT. Any 3-SAT clause $$(x_1 \lor x_2 \lor x_3)$$ can be rewritten into the equisatisfiable 2-SAT-with-XOR-relations 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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ All answers seem to be correct or assisting, but I found this one the most elegant (imho). $\endgroup$
    – Albert Hendriks
    Commented May 14, 2015 at 9:19
  • 1
    $\begingroup$ Nice answer. It may be worth mentioning that mere equisatisfiability would not be enough here (since the satisfying assignments of the expressions corresponding to all the clauses of a satisfiable CNF might not match), but your rewritten expression actually has a corresponding satisfying assignment for each satisfying assignment of the original clause. $\endgroup$
    – Klaus Draeger
    Commented May 15, 2015 at 12:52
7
$\begingroup$

You haven't specified the arity of your XOR relations, but like in the usual SAT-to-3SAT reduction, you can always arrange that their arity be at most 3. Now you are in great position to apply Schaefer's dichotomy theorem, which will tell you whether your problem is in P or NP-complete (these are the only two options). If it turns out to be in P, the next step could be looking at Allender et al., which will let you know how easy your problem is.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This doesn't take into account the condition that there are $O(n)$ constraints, but you can always add dummy variables to ensure that the condition is satisfied. $\endgroup$
    – Yuval Filmus
    Commented May 13, 2015 at 17:46
5
$\begingroup$

By Schaefer's dichotomy theorem, this is NP-complete.

Consider the case where all clauses have 2 or 3 literals in them; then we can consider this as a constraint satisfaction problem over a set $\Gamma$ of relations of arity 3. In particular, the relations $R(x,y,z)$ are the following: $x \lor y$, $x \lor \neg y$, $\neg x \lor \neg y$, $x \oplus y \oplus z$, $x \oplus y \oplus \neg z$.

Now apply Schaefer's dichotomy theorem, in its modern form. Check each of the six operations to see if they are a polymorphism:

  • Unary 0: Not a polymorphism of $x \lor y$.
  • Unary 1: Not a polymorphism of $\neg x \lor \neg y$.
  • Binary AND: Not a polymorphism of $x \lor y$. (Consider $(0,1,0)$ and $(1,0,0)$; they both satisfy the relation, but their pointwise-AND $(0,0,0)$ doesn't.)
  • Binary OR: Not a polymorphism of $\neg x \lor \neg y$. (Consider $(0,1,0)$ and $(1,0,0)$; they satisfy the relation, but $(1,1,0)$ doesn't.)
  • Ternary majority: Not a polymorphism of $x \oplus y \oplus z$. (Consider $(0,0,1)$ and $(0,1,0)$ and $(1,0,0)$; they satisfy the relation, but their majority $(0,0,0)$ doesn't.)
  • Ternary minority: Not a polymorphism of $x \lor y$. (Consider $(0,1,0)$, $(1,0,0)$, and $(1,1,0)$; they satisfy the relation, but their minority $(0,0,0)$ doesn't.)

It follows that this problem is NP-complete, even if you restrict all the XOR clauses to be of length at most 3.

On the other hand, if all the XOR clauses are restricted to be of length at most 2, then this is in P. In particular $(x \oplus y)$ is equivalent to $(x \lor y) \land (\neg x \lor \neg y)$, so any such formula is equivalent to a 2SAT formula, whose satisfiability can be determined in polynomial time.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.