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.
Conversion between k-SAT and XOR-SAT
sat;boolean functions;boolean formulas
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 ValiantVazirani 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.