8
$\begingroup$

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.

$\endgroup$
  • 5
    $\begingroup$ 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. $\endgroup$ – Tsuyoshi Ito Nov 9 '14 at 1:23
  • 1
    $\begingroup$ In particular $x \lor y$ has no equivalent XOR-SAT formula. $\endgroup$ – Huck Bennett Nov 9 '14 at 4:34
  • $\begingroup$ @TsuyoshiIto, agreed. I think I should have assumed a promise that the $k$-SAT expressions have equivalent XOR-SAT expressions. Updating the question. $\endgroup$ – Omar Shehab Nov 9 '14 at 9:05
  • $\begingroup$ @HuckBennett, I have added a promise in the question. $\endgroup$ – Omar Shehab Nov 9 '14 at 9:08
  • 1
    $\begingroup$ I see, that makes the problem interesting! $\endgroup$ – Tsuyoshi Ito Nov 10 '14 at 5:49
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Omar Shehab Nov 10 '14 at 15:17
  • $\begingroup$ Can we say that Davis-Putnam-Logemann-Loveland algorithm is by far the best known result for this? $\endgroup$ – Omar Shehab Nov 11 '14 at 11:22
  • 2
    $\begingroup$ 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. $\endgroup$ – Kyle Jones Nov 11 '14 at 15:15
  • $\begingroup$ Doesn't $\mathsf{P=UP}$ imply $\mathsf{P=NP}$? $\endgroup$ – rus9384 Sep 13 '17 at 18:50
  • $\begingroup$ @rus9384 Not necessarily. See If one shows that UNIQUE k-SAT is in P, does it imply P=NP? $\endgroup$ – Kyle Jones Sep 13 '17 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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