I have a large system of $3$-$XORSAT$ constraints (i.e. up to $3$ variables per constraint) and this can be represented in matrix form as a linear algebra problem $Ax=b$ $mod$ $2$. Solvability (i.e. the satisfiability of the $3$-$XORSAT$ system) can be tested by using Gaussian elimination which involves multiple rounds of matrix multiplication. As far as I am aware this is the only/standard approach.
For large systems this seems rather wasteful both in terms of storage (i.e. the matrix $A$ contains mostly zeros) and in terms of computation (i.e. a lot matrix multiplication involving mainly $0$ entries). Given that all entries in $A$, $x$ and $b$ are in a binary field $GF(2)$, I wondered if there might be a more efficient way of storing and solving such a system.
Are there any representations and/or algorithms (other than using a sparse matrix $A$ and Gaussian elimination) that are specifically suited to solve large $3$-$XORSAT$ instances?
I have been searching for literature that addresses this question of solving (very) sparse matrices over small fields and amongst others found the following interesting (albeit old) paper : http://i.stanford.edu/pub/cstr/reports/na/m/80/06/NA-M-80-06.pdf Although this paper does not explicitly mention small fields, it presents an interesting idea of using pointers to keep track of just the the non-zeros (and thus eliminates the use of a large sparse matrix $A$). I was thinking of implementing something using this proposed idea, but explicitly for binary values, which further simplifies the computational effort. Am I re-inventing the wheel?
Any ideas or suggestions are welcome.
Based on the comments I have added the following further observations:
One of the well known boolean satisfiability solvers that implements XORSAT as part of its algorithm is CryptoMiniSat (see @KyleJones comment below). A description of how it implements $XORSAT$ can be found here (see sections 5 and 6): https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.636.6082&rep=rep1&type=pdf
CryptoMiniSat is explicitly NOT using a sparse representation of matrix $A$, but has opted to 'densify' the matrix by bundling column entries together in bit-vectors and using row-by-row $XOR$ operations on these bit-vectors. This reduces the storage requirement of the matrix $A$ by a factor $n$ (where $n$ is the size of the bit-vector). It would be interesting to hear from someone who has detailed knowledge of the CryptoMiniSat algorithm on why sparse representations were rejected in the design. It suggests in the linked paper above that in practice matrix $A$ is simply not sufficiently large or sparse when dealing with a generic satisfiability problem. It does reference this paper (<https://epubs.siam.org/doi/10.1137/0613024 >), which explains that MATLAB uses an (optional) sparsification method for its matrix functions (including Gaussian elimination). However, the approach is very generic and is not tailored to the binary field $GF(2)$.
As @YuvalFilmus has pointed out, any $XORSAT$ formula (including those that are represented by a dense matrix $A$) can be converted to a $3$-$XORSAT$ formula (which, by definition, corresponds to a sparse matrix $A$). Therefore it is indeed unlikely that there is an algorithm that always outperforms Gaussian elimination.
AFAICT, the method that is using a pointer based approach (see paper linked above) does not resolve the issue of potential back-fill of non-zero entries (i.e. backfill results in an expansion of the storage requirement). Unless a convenient order of rows and columns can be chosen to minimize this issue, a $3$-$XORSAT$ formula representing a dense $XORSAT$ formula might end up taking up more space and be less computationally efficient than using the full matrix representation. The question remains though if, on average, a sparse representation comes out better.
Given that we are dealing with the binary field $GF(2)$, the factor graph of the $3$-$XORSAT$ system may have a role to play; either by allowing the optimization of the order of rows/columns to limit back-fill, or even by sidestepping Gaussian elimination altogether.