I have $m$ equations of the following form: $$x_1+x_2+\cdots+x_n=s,$$ where each variable is either 1 or 0, and the total number of variables is $m\approx3{,}000$. So I’m thinking of modeling each variable as a binary variable and each equation as a CNF formula so that, once I combine all formulas into one CNF, I can solve it using a SAT solver.

I’ve tried to solve the system of equations using Gaussian elimination, but it was too slow since the time complexity is $m^3\approx27{,}000{,}000{,}000$.

My problem is how to encode addition efficiently and simply. My only known approach is to model $a+b$ as a circuit and then convert the big totality of $n$ circuits to a CNF. Is there a better way?

  • 1
    $\begingroup$ Are the equations modulo 2 or in the integers? I doubt that a SAT solver will be faster than Gaussian elimination. Have you tried optimized implementations of matrix inversion, e.g., BLAS/LAPACK? $\endgroup$
    – D.W.
    Commented Jun 13, 2020 at 7:48
  • 1
    $\begingroup$ See also mathworld.wolfram.com/StrassenFormulas.html, cs.stackexchange.com/q/83289/755, cs.stackexchange.com/q/60897/755, $\endgroup$
    – D.W.
    Commented Jun 13, 2020 at 7:56
  • $\begingroup$ @D.W. Not modulo 2; additions are usual integer additions. I’m going to try both. Thanks for the hints. $\endgroup$
    – Zirui Wang
    Commented Jun 13, 2020 at 10:19


Your Answer

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