# 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?