# Why is it useful to transform 0-1 integer programming problem into SAT problem?

There are several researches studying translating 0-1 integer programming into CNF form. For example, this paper and this C++ library. As the lecture notes here goes, translating 0-1 integer programming problem into CNF form might introduce $$O(n\log^2 n)$$ extra variables. However, it seems that the time complexity of solving satisfiability problem is connected to the number of variables. For example, to my best knowledge, the fastest algorithm to solve 3-SAT problem has time complexity about $$O(1.3^n)$$ which is to the power of $$n$$. Therefore, if we introduce $$n\log^2 n$$ more auxiliary variables, the time complexity of solving the 0-1 integer programming problem may be kind of like $$O(c^{2n}n^{\log n})$$, which seems to be a huge cost. Also, the time complexity of the translating process might also be taken into consideration. I was wondering if it is still efficient to transform the 0-1 integer programming first rather than using other tools, for example, this paper to solve it directly.

I am new to theory of satisfiability and its connection to 0-1 integer programming. I do apologize that this question might be trivial. Thanks for any help!