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?
