patternModerate
Is 2-SAT with XOR-relations NP-complete?
Viewed 0 times
satxorrelationswithcomplete
Problem
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:
-
XOR part :
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.
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.
Solution
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.
Context
StackExchange Computer Science Q#42502, answer score: 12
Revisions (0)
No revisions yet.