Re: Solve math inequelity with SAT resulotion

In article <99799$453dfb99$839b6494$5558@xxxxxxxxxxxxxxxx>,
MadMocro (chuchu_w@xxxxxxxxxxx) 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.

If you enter

Reduce[{2 a > b + c, 2 b > c + d, 2 c > 3 d, 3 d > a + c},
{a, b, c, d}, Integers]

into Mathematica, you get the general solution to this problem:

Element[(C[1] | C[2] | C[3] | C[4]), Integers] &&
C[1]?0 && C[2]?0 && C[3]?0 && C[4]?0 &&
a == 11 C[1]+10 C[2]+6 C[3]+3 C[4]+30 &&
b == 10 C[1]+9 C[2]+5 C[3]+3 C[4]+27 &&
c == 12 C[1]+11 C[2]+6 C[3]+3 C[4]+32 &&
d == 8 C[1]+7 C[2]+4 C[3]+2 C[4]+21

Here the C[i] are arbitrary non-negative integers.

Cheers,
Paul

_______________________________________________________________________
Paul Abbott Phone: 61 8 6488 2734
School of Physics, M013 Fax: +61 8 6488 1014
The University of Western Australia (CRICOS Provider No 00126G)
AUSTRALIA http://physics.uwa.edu.au/~paul
.