<p>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.</p>

<p>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.</p>

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

<p>$a \oplus b \oplus c$</p>

<p>to</p>

<p>$
\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
$</p>

<p>this <a href="http://www.msoos.org/2011/03/recovering-xors-from-a-cnf/">can be done in polynomial time</a> by sorting the clauses followed by a linear-time scan.</p>

CC BY-SA 3.0
2014-11-10T15:17:28.530Z
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.
Omar Shehab
CC BY-SA 3.0
2014-11-11T11:22:58.753Z
Can we say that Davis-Putnam-Logemann-Loveland algorithm is by far the best known result for this?
Omar Shehab
CC BY-SA 3.0
2014-11-11T15:15:33.997Z
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.
Kyle Jones
CC BY-SA 3.0
2017-09-13T18:50:03.413Z
Doesn't $\mathsf{P=UP}$ imply $\mathsf{P=NP}$?
rus9384
CC BY-SA 3.0
2017-09-13T20:44:37.140Z
@rus9384 Not necessarily.  See [If one shows that UNIQUE k-SAT is in P, does it imply P=NP?](https://cs.stackexchange.com/questions/33225/if-one-shows-that-unique-k-sat-is-in-p-does-it-imply-p-np/)
Kyle Jones
CC BY-SA 3.0
2014-11-10T05:23:25.677Z
2014-11-10T05:23:25.677Z
Kyle Jones
<p>According to <a href="http://www.cs.sfu.ca/~mitchell/cmpt-417/2011-Spring/Project-Readings/lait10xor.pdf">XOR Satisfiability Solver Module for DPLL Integration</a> 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.</p>

<p>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.</p>

CC BY-SA 3.0
2014-11-09T01:23:41.853Z
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.
Tsuyoshi Ito
CC BY-SA 3.0
2014-11-09T04:34:46.353Z
In particular $x \lor y$ has no equivalent XOR-SAT formula.
Huck Bennett
CC BY-SA 3.0
2014-11-09T09:05:05.270Z
@TsuyoshiIto, agreed. I think I should have assumed a promise that the $k$-SAT expressions have equivalent XOR-SAT expressions. Updating the question.
Omar Shehab
CC BY-SA 3.0
2014-11-09T09:08:19.967Z
@HuckBennett, I have added a promise in the question.
Omar Shehab
CC BY-SA 3.0
2014-11-10T05:49:45.750Z
I see, that makes the problem interesting!
Tsuyoshi Ito
<sat><boolean-functions><boolean-formulas>
Conversion between k-SAT and XOR-SAT
Omar Shehab
# Conversion between k-SAT and XOR-SAT

(Asked by: username_0 on 2014-11-08)

According to [XOR Satisfiability Solver Module for DPLL Integration](http://www.cs.sfu.ca/~mitchell/cmpt-417/2011-Spring/Project-Readings/lait10xor.pdf) 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.

**Tags:** sat, boolean-functions, boolean-formulas

> **Comments:**
> **username_1**: 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.  
> **username_2**: In particular $x \lor y$ has no equivalent XOR-SAT formula.  
> **username_0**: @TsuyoshiIto, agreed. I think I should have assumed a promise that the $k$-SAT expressions have equivalent XOR-SAT expressions. Updating the question.  
> **username_0**: @HuckBennett, I have added a promise in the question.  
> **username_1**: I see, that makes the problem interesting!  

---

## 1 answers

### Answer by username_3 on 2014-11-10. Score: 6 | Accepted answer

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](http://www.msoos.org/2011/03/recovering-xors-from-a-cnf/) by sorting the clauses followed by a linear-time scan.

> **Comments:**
> **username_0**: 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.  
> **username_0**: Can we say that Davis-Putnam-Logemann-Loveland algorithm is by far the best known result for this?  
> **username_3**: 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.  
> **username_4**: Doesn't $\mathsf{P=UP}$ imply $\mathsf{P=NP}$?  
> **username_3**: @username_4 Not necessarily.  See [If one shows that UNIQUE k-SAT is in P, does it imply P=NP?](https://cs.stackexchange.com/questions/33225/if-one-shows-that-unique-k-sat-is-in-p-does-it-imply-p-np/)  

---

