Poly-time reduction from ILP to SAT?

Question

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?

Answer 1

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.

Answer 2

It is some sort of necro-answer to already answered and accepted question, but I want to note, that there is really easier way.

Consider you have one of inequalities like this:

$5*x_1 + 2*x_2 + 3*x_3 \leq 6$

You may easily test all no-vectors for this inequality: $(1, 1, 1)$, $(1, 1, 0)$ and $(1, 0, 1)$ others are ok.

First vector $(1, 1, 1)$ means that all three can not be true: $\neg(x_1 \land x_2 \land x_3)$ and we may rewrite this as a disjunct $(\neg x_1 \lor \neg x_2 \lor \neg x_3)$.

This way you may form 3 clauses from no-vectors: $(\neg x_1 \lor \neg x_2 \lor \neg x_3)$, $(\neg x_1 \lor \neg x_2 \lor x_3)$ and $(\neg x_1 \lor x_2 \lor \neg x_3)$

Traversing all inequalities and collecting clauses you will get cnf in the end. Often this cnf will be WAY SIMPLER, then one, that results from accepted answer. Cost is harder pre-processing, though.