# Conversion between k-SAT and XOR-SAT

According to XOR Satisfiability Solver Module for DPLL Integration by Tero Laitinen, we need $2^{n-1}$ CNF clauses to convert an $n$ literal XOR-SAT clause if we do not want to increase the number of literals. So, I understand that the computational cost for converting an XOR-SAT expression into a strictly CNF $k$-SAT is exponential.

My question: What is the computational cost if I want to reverse the process? What is the computational cost of converting a CNF $k$-SAT expression into an XOR-SAT one? I assume the promise that in this case only the $k$-SAT expressions with equivalent XOR-SAT expressions are considered.

• Isn’t it clearly impossible in the worst case? Some CNF formulas are not affine, so they cannot be represented as a conjunction of XOR clauses. Commented Nov 9, 2014 at 1:23
• In particular $x \lor y$ has no equivalent XOR-SAT formula. Commented Nov 9, 2014 at 4:34
• @TsuyoshiIto, agreed. I think I should have assumed a promise that the $k$-SAT expressions have equivalent XOR-SAT expressions. Updating the question. Commented Nov 9, 2014 at 9:05
• @HuckBennett, I have added a promise in the question. Commented Nov 9, 2014 at 9:08
• I see, that makes the problem interesting! Commented Nov 10, 2014 at 5:49

If all XOR relationships between variables in CNF formulas could be detected in polynomial time, then this would allow the solution of UNAMBIGUOUS-SAT in polynomial time. By the Valiant–Vazirani theorem this result would imply that NP = RP.

To solve UNAMBIGUOUS-SAT, recall that $a \oplus b$ implies $a \neq b$. Find the XOR relationship between each pair of variables and use the results to divide the variables into two groups of equivalent variables. Once this is done, only two test assignments are required to determine satisfiability.

In the limited case of recovering XOR relationships encoded in the usual way, i.e.

$a \oplus b \oplus c$

to

$\lnot a \lor b \lor c \\ a \lor \lnot b \lor c \\ a \lor b \lor \lnot c \\ \lnot a \lor \lnot b \lor \lnot c$

this can be done in polynomial time by sorting the clauses followed by a linear-time scan.

• thanks. I would like to know the complexity of converting a CNF expression into an XOR-SAT expression. I assume that we are considering those CNF expressions for which there are equivalent XOR-SAT expressions. Commented Nov 10, 2014 at 15:17
• Can we say that Davis-Putnam-Logemann-Loveland algorithm is by far the best known result for this? Commented Nov 11, 2014 at 11:22
• Unless NP=RP (a miraculous result) divining XOR relationships will require exponential time in the general case. This is independent of the SAT solving algorithm used. Commented Nov 11, 2014 at 15:15
• Doesn't $\mathsf{P=UP}$ imply $\mathsf{P=NP}$? Commented Sep 13, 2017 at 18:50
• @rus9384 Not necessarily. See If one shows that UNIQUE k-SAT is in P, does it imply P=NP? Commented Sep 13, 2017 at 20:44