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!


One important thing to know about ILP and 3SAT is that, often, on problem instances that arise on practice, they can be solved faster than a worst-case analysis would indicate. As such, worst-case running time analysis isn't necessarily predictive of what you'll see in practice.

Your big-O running times reflect worst-case running time of certain algorithms. The worst case is certainly terrible. However, off-the-shelf ILP solvers and SAT solvers have heuristics that sometimes do significantly better -- though their worst case remains terrible.

So, if you care about worst-case running times, converting to CNF might not be the best approach. But if you care about practical solutions, you could try either using an ILP solver, or you could try converting to CNF and using a SAT solver. Depending on the problem, it is possible that either might be effective, or that neither one is effective.

  • $\begingroup$ Thanks for answering! Is it correct to say that either approach only stands out when solving certain kinds of problem and its performance (time complexity), in general, is not very predictable? $\endgroup$
    – Slangevar
    Jun 29 at 8:34
  • 1
    $\begingroup$ @Slangevar, yes, that's correct. $\endgroup$
    – D.W.
    Jun 29 at 9:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.