9
$\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.

Improve this question
$\endgroup$
5
  • 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, 2014 at 1:23
  • 1
    $\begingroup$ In particular $x \lor y$ has no equivalent XOR-SAT formula. $\endgroup$
    – Huck Bennett
    Nov 9, 2014 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, 2014 at 9:05
  • $\begingroup$ @HuckBennett, I have added a promise in the question. $\endgroup$
    – Omar Shehab
    Nov 9, 2014 at 9:08
  • 1
    $\begingroup$ I see, that makes the problem interesting! $\endgroup$
    – Tsuyoshi Ito
    Nov 10, 2014 at 5:49

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
5
  • $\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, 2014 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, 2014 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, 2014 at 15:15
  • $\begingroup$ Doesn't $\mathsf{P=UP}$ imply $\mathsf{P=NP}$? $\endgroup$
    – rus9384
    Sep 13, 2017 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, 2017 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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