1
$\begingroup$

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:

  1. 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

  2. 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)$.

  3. 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.

  4. 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.

  5. 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.

$\endgroup$
8
  • $\begingroup$ You can reduce XORSAT to 3XORSAT in the same way that you reduce SAT to 3SAT. $\endgroup$ May 1 at 18:48
  • $\begingroup$ Look into CryptoMiniSat if you haven't already. It is an open-source SAT solver that implements Gauss-Jordan elimination for XORSAT as a part of its general solver. I haven't looked at its source code to see if it has interesting optimizations in this area but I would be surprised if it didn't. $\endgroup$
    – Kyle Jones
    May 1 at 19:19
  • $\begingroup$ @YuvalFilmus, do you mean reducing the number of variables (or columns in matrix A) by iteratively propagating unit-XOR clauses and replacing variables in 2-XOR clauses to end up with a system with only 3-XOR clauses? $\endgroup$
    – scobiem
    May 1 at 21:55
  • $\begingroup$ @KyleJones, thanks for the suggestion. I am fairly familiar with cryptominisat, but haven't looked at the source code (yet). There is a fairly good explanation in this paper <citeseerx.ist.psu.edu/viewdoc/…> on how Gaussian elimination is implemented (see sections 5&6). AFAIKT it still very much relies on Gaussian elimination but with variables being bundled together in bit-vectors to allow XOR operations at the CPU level. $\endgroup$
    – scobiem
    May 1 at 22:12
  • 1
    $\begingroup$ You can transform any XORSAT instance to a 3XORSAT instance of similar size. In other words, I don’t expect 3XORSAT to be any easier than XORSAT. $\endgroup$ May 2 at 4:01

0

Your Answer

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

Browse other questions tagged or ask your own question.