Reducing Zero-One Integer Linear Programming problem to SAT

Question

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$

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.

Answer 1

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.

Answer 2

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.