Re: Solve math inequality with SAT (CNF)

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
.