6

XOR Formulas

Consider boolean formulas with connectives $\wedge$ (AND) and $\oplus$ (XOR). Such a boolean formula is a valid instance for XOR SAT if it is a conjunction of $\oplus$-clauses. An $\oplus$-clause contains literals that are connected with $\oplus$.

Example Formula:

$(v_1 \oplus \bar{v_2} \oplus v_3 \oplus v_4) \wedge (\bar{v_1} \oplus v_2) \wedge (\bar{v_2} \oplus v_3 \oplus \bar{v_4})$

Decision Problem

Name: XOR 3-SAT

Input: A boolean formula that is a conjunction of $\oplus$-clauses where each clause contains three literals.

Question: Does there exist an assignment to the variables that satisfies the formulas?

More Background

XOR SAT can be reduced to solving a system of equations over $\mathbb{Z}_2$. This is because every $\oplus$-clause can be thought of as an equation. As a result, XOR SAT is solvable in polynomial time using gaussian elimination.

Further, XOR 2-SAT can be reduced to solving reachability in an undirected graph. This is because every $\oplus$-clause with two literals defines an edge in an undirected graph. As a result, XOR 2-SAT is solvable in logspace because reachability in an undirected graph is solvable in logspace (because SL = L).

Question

(1) Is XOR 3-SAT solvable in logspace?

(2) Are there any known consequences of solving XOR 3-SAT in logspace?

(3) For example, would this imply that XOR $k$-SAT is solvable in logspace?

Michael Wehar
  • 5,127
  • 1
  • 24
  • 54
  • A related post: https://cstheory.stackexchange.com/questions/36704/xor-sat-to-horn-sat-reduction/36876 – Michael Wehar Jun 30 '18 at 00:14
  • @user124864 I'm not entirely sure. – Michael Wehar Jun 30 '18 at 00:58
  • I just found this which I think is relevant: https://cstheory.stackexchange.com/questions/8936/is-solving-systems-of-equations-modulo-k-in-mathsfcomod-k-mathsf-l-for-k – Michael Wehar Jun 30 '18 at 00:58
  • 2
    There is an obvious reduction of XOR-SAT to XOR-3-SAT. Both problems are $\oplus L$-complete, hence you are simply asking about the consequences of $L=\oplus L$. Oh, and of course $\oplus L\subseteq NC^2\subseteq DSPACE((\log n)^2)$ – Emil Jeřábek Jun 30 '18 at 12:24

1 Answers1

13

Take a look at https://www.sciencedirect.com/science/article/pii/S0022000008001141 "The complexity of satisfiability problems: Refining Schaefer's theorem" by Allender et al. which answer your questions:

(1) Open

(2) $\oplus L = L$

(3) Yes

Gustav Nordh
  • 1,047
  • 8
  • 16
  • 1
    Thank you so much!! This is exactly what I wanted!! I didn't initially realize that we could reduce XOR SAT to XOR 3-SAT using the same trick as we do for reducing CNF SAT to CNF 3-SAT. Also, reference [28] from the paper that you linked explains why XOR SAT is $\oplus L$ complete. – Michael Wehar Jun 30 '18 at 13:10