Solve math inequality with SAT (CNF)

Hello,

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.

Thanks in advance.

Madmocro



--
--------------------------------- --- -- -
Posted with NewsLeecher v3.7 Final
Web @ http://www.newsleecher.com/?usenet
------------------- ----- ---- -- -

.

Relevant Pages

  • Solve math inequelity with SAT resulotion
    ... I have a SAT problem that is giving me headache. ... problem that has to be solved with SAT resolution. ... how I can convert integers and math inequalities into Boolean or CNF ... The problem is to find (positive integers) values a,b,c,d such ...
    (sci.math.symbolic)
  • Re: Solve math inequelity with SAT resulotion
    ... problem that has to be solved with SAT resolution. ... how I can convert integers and math inequalities into Boolean or CNF ... The problem is to find (positive integers) values a,b,c,d such ... ILP encoding into SAT and there are two well know encodings: ...
    (sci.math.symbolic)
  • Re: Find out if I/10^i = J/2^j (decadic - dyadic pairing)
    ... study some discrete mathematics or number theory. ... "math boot camp" during my bachelory for math linguistics, ... Given known positive integers I and i and unknown positive integers J ...
    (sci.math)
  • Re: number theory
    ... prime numbers form other positive integers ... Capitalization and spaces as described is how English and Spanish are both ... Now as math is exacting, your sloppy writing style demonstrating ...
    (sci.logic)
  • Re: [patch] hrtimer: round up relative start time on low-res arches
    ... On Wed, 15 Feb 2006, Ingo Molnar wrote: ... whole of m68k wont be penalized via CONFIG_TIME_LOW_RES for having a ... resolution timer - every clock can define its own resolution. ... math and code to keep it cheap and simple, ...
    (Linux-Kernel)