I want to find a reduction from Zero-One Integer Linear Programming problem to Boolean Satisfiability problem (SAT), that is, to find a polynomial-time transformation $T$, such that: $$IP \leq_P SAT$$ $$IP(in_{IP}) = 1 \iff SAT(T(in_{IP})) = 1$$ where $in_{IP}$ is an input for the IP problem and $T(in_{IP}) = in_{SAT}$ is a boolean formula (input for the SAT problem).

First, I have considered a particular case for IP, where $$x_1 +x_2 + \cdots +x_n \leq p$$ $$x_i = 0 \ \text{or} \ x_i = 1, \ \forall i =1..n, \ \forall p \geq0 $$ Translated into boolean language, the transformation will construct a formula where at most p variables must be set to true for the formula to be satisfiable.

Next, I've considered a concrete example, constructing the following ROBDD that allowed me to express the following inequality: $$x_1 + x_2 + x_3 \leq 2$$ $\hskip 2.5in$ robdd

where continuous arrow means 1 and dotted arrow means 0. I have also invented the variabiles $x_i\_$ that somehow mirrors the behaviour of $x_i$ sub-component (i.e. swaps routes).

Now, is there a way I can formalize this whole process, that is, express the concept of at most in boolean algebra language? I think this is the key to find the actual transformation.

  • $\begingroup$ this is a standard reduction originally done in a scientific paper somewhere, might try to dig it up if there is interest $\endgroup$
    – vzn
    Aug 4, 2016 at 16:24
  • $\begingroup$ I have seen reductions from SAT to 0-1 ILP, but have not found something related to the inverse transformation. $\endgroup$ Aug 4, 2016 at 17:16
  • $\begingroup$ aha it looks like its in Karps original 21 problems $\endgroup$
    – vzn
    Aug 4, 2016 at 17:47

2 Answers 2


The existence of such a reduction follows immediately from the Cook-Levin theorem, which guarantees that you can reduce any problem in NP to SAT and describes explicitly one way to do it. Just work through the steps of the proof of the theorem (which can be found in any textbook) and you'll obtain a valid reduction from 0-1 ILP to SAT.

  • $\begingroup$ seems like circular ref to me. how do you know 0-1 ILP is NP complete? that seems the essence of the question. $\endgroup$
    – vzn
    Aug 4, 2016 at 17:49
  • 4
    $\begingroup$ @vzn, it's not circular. The question doesn't ask whether 0-1 ILP is NP-complete. You don't need to know 0-1 ILP is NP-complete to apply the Cook-Levin theorem. The Cook-Levin theorem applies to all problems that are in NP (whether NP-complete or not)... and 0-1 ILP is certainly in NP. $\endgroup$
    – D.W.
    Aug 4, 2016 at 19:25

There are two variants to perform the encoding. I am assuming that you want the SAT instance in Conjunctive Normal form, as otherwise your ROBDD can be mapped pretty directly to a Boolean formula of size (but not length) linear in the number of variables.

In variant 1, we do not want to introduce additional variables. Essentially, we want to add clauses that rule out all paths in the ROBBD that lead to the "0" node. So if $x_1 + x_2 + x_3 \leq 2$, this would be only one clause, namely $\neg x_1 \vee \neg x_2 \vee \neg x_3$. For translating $x_1 + x_2 + x_3 \leq 1$, there are four different paths in the ROBBD to the "0" node. Encoding the paths yields $\neg x_1 \vee \neg x_2 \vee \neg x_3$, $\neg x_1 \vee \neg x_2 \vee x_3$, $x_1 \vee \neg x_2 \vee \neg x_3$ as clauses, which can be simplified to $\neg x_1 \vee \neg x_2$, $\neg x_2 \vee \neg x_3$, $\neg x_1 \vee x_3$. Note that the number of clauses necessary for this encoding can be exponential in the number of variables employed in the inequality, so this encoding is not always suitable.

In variant 2, we introduce additional variables to the SAT problem to help us with the encoding. For example, we can introduce for the every ROBDD node a SAT variable and then encode which path through the ROBDD the assignment to $x_1, x_2, x_3$ takes. Example:

  • $v_1$
  • $\neg v_1 \vee \neg x_1 \vee v_2$
  • $\neg v_1 \vee x_1 \vee v_T$
  • $\neg v_2 \vee \neg x_2 \vee v_3$
  • $\neg v_2 \vee x_2 \vee v_T$
  • $\neg v_3 \vee \neg x_3 \vee v_F$
  • $\neg v_3 \vee x_3 \vee v_T$
  • $v_T$
  • $\neg v_F$

The added $v$ variables represent which node in the ROBDD is reached. Note that this example is not built after your ROBDD, as it does not represent $x_1 + x_2 + x_3 \leq 2$, as it maps $x_1 = 0$, $x_2 = 1$, $x_3 = 0$ to $0$.

The nice property of variant 2 above is that the encoding is only linear in the size of the ROBDD, which in turn is at most quadratic in the number of variables employed in the inequality. But note that there are also many other possible encodings of the linear inequality into SAT. The paper ``PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF'' contains some pointers.

  • $\begingroup$ What is the ROBDD? $\endgroup$
    – Jxb
    Jul 4, 2023 at 9:34
  • $\begingroup$ @Jxb A ROBDD is a "Reduced Ordered Binary Decision Diagram" $\endgroup$
    – DCTLib
    Jul 4, 2023 at 10:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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