Poly-time reduction from ILP to SAT?

Problem Detail: 

So, as is known, ILP's 0-1 decision problem is NP-complete. Showing it's in NP is easy, and the original reduction was from SAT; since then, many other NP-Complete problems have been shown to have ILP formulations (which function as reductions from those problems to ILP), because ILP is very usefully general.

Reductions from ILP seem much harder to either do myself or track down.

Thus, my question is, does anyone know a poly-time reduction from ILP to SAT, that is, demonstrating how to solve any 0-1 ILP decision problem using SAT?

Asked By : codetaku

Answered By : Realz Slaw

0-1 ILP formulated as:

Does there exist a vector $\mathbf{x}$, subject to constraints:

$$ \left.\begin{array}{rrrrr|rr} a_{11} x_1 & + &a_{12} x_2 & ... + & a_{1n} x_n\le b_1 \\ a_{21} x_1 & + &a_{22} x_2 & ... + & a_{2n} x_n\le b_2 \\ ...\\ a_{m1} x_1 & + &a_{m2} x_2 & ... + & a_{mn} x_n\le b_m \\ \end{array}\right. $$

Domain of x: $\forall_{x_j \in \mathbf{x}} x_j\in \{0,1\}$

Reduction to k-sat:

First reduce to circuit sat:

Start with the first row, create a boolean variable for representing each bit in $a_{1j}$ and one boolean variable for $x_j$. Then make variable for $b_1$. Make an addition circuit (pick your favorite) adding the row up.

Then make a comparison circuit, declaring the sum to less than $b_1$.

Convert these two circuits to CNF, filling in the $a_{1j}$ variables and $b_1$ since they are given.

Repeat for all rows, but reuse the $x_j$ variables between them.

The final CNF will contain all the constraints.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/16088