Re: ILP ==> 0,1 ILP ==>SAT

I want the reduction from ILP to SAT for the following three reasons:

First, SAT can be done in circuit and more intuitive than ILP for a
programmer like me,

Second, I have got a very fast SAT algorithm and want to use it to solve ILP
problem, my real target in real application,

Third, if SAT is solved, we need the reduction to make use of the polynomial
SAT algorithm.


Thanks,

Thomas Li





"Keith Ramsay" <kramsay@xxxxxxx> wrote in message
news:1119723449.982836.69800@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> Thomas A. Li wrote:
> |Does anybody has any information about:
> |
> |a polynomial reduction of ILP, integer linear programming, without
> |minimization/maximization
> |to 0,1 ILP and/or
> |finally to SAT in Boolean Logic?
>
> The opposite reductions are of course much more familiar,
> since they're used to show that ILP is NP-hard.
>
> I don't remember seeing it proven that the decision problem
> for ILP is in NP, although if you can reduce it to SAT then
> I suppose it is. The only real issue as far as I can see is
> proving that one can put reasonable bounds on the variables
> without turning a feasiable problem into an unfeasible one.
> By reasonable I mean that the number of bits has to be a
> polynomial in the size of the original problem, which is
> quite generous.
>
> The kind of reduction you want depends a lot on what you
> want it for. If your purpose is only theoretical, then it
> might be easiest to apply the reduction in the proof of
> Cook's theorem to show that ILP reduces to SAT, and then
> Karp's reduction used to prove the 0,1-ILP decision problem
> is NP-complete to reduce SAT to 0,1-ILP. Applying Cook's
> theorem depends upon being able to put reasonable bounds
> on the variables.
>
> If you want the reductions for some other purpose, maybe
> you should elaborate.
>
> Keith Ramsay
>


.