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?