Re: Solve math inequality with SAT (CNF)

The problem tha you have can be represented as a linear programming
problem.Fortunately LP lie in the class P,unfortunately in case that
you have constrains over integers(which is more to contiguous to your
problem) the problem is called Integer Linear Programming which is
NP-complete.The completeness is from 0-1 linear programming,and O-1 LP
is trivially reducible in SAT.Find in the net,see Papadimitriou
Computational Complexity,Papadimitriou&Steiglitz Combinatorial
Optimization,etc .Is not that complex..
The "partial order" of problems is:SAT<0-1LP<ILP.
so you represent your problem as ILP and start the reductions in order
to achieve the ¨equivalent¨ SAT expression.(The reductions are well
defined polynomial procedures and informally make a mapping from one
problem instance to another).

Over the net there is a plethora of tutorials that can help you.
My apologies in case that i wrote is mistaken and not well defined.
Feel free to contact in case you need something more exact..
tchow@xxxxxxxxxxxxx wrote:
In article <885d7$453dfaaf$839b6494$5555@xxxxxxxxxxxxxxxx>,
mehassan@xxxxxxxxxxx <MadMocro> wrote:
I have a SAT problem that is giving me headache. It is a math
problem that has to be solved with SAT resolution. But I don't see
how I can convert integers and math inequalities into Boolean or CNF
form. The problem is to find (positive integers) values a,b,c,d such
that 2a > b + c and 2b > c + d and 2c > 3d and 3d > a+ c. I don't
see how I can turn this into a CNF. specially the ">" and "+".
I'm still a beginner so have some mercy. I'm not asking for a
complete solution but some hints and guidance in the right direction
or just and small example.

Represent the integers in binary, and create a Boolean variable for
each binary digit of each integer. Then think about how you would
explain, to a computer that can deal with only a couple of bits at
a time, how to tell which of two binary integers is larger.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences

.