# CNF encoding of additions

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?

• 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? – D.W. Jun 13 '20 at 7:48
• – D.W. Jun 13 '20 at 7:56
• @D.W. Not modulo 2; additions are usual integer additions. I’m going to try both. Thanks for the hints. – Zirui Wang Jun 13 '20 at 10:19