Re: Solve math inequelity with SAT resulotion
- From: pocmatos@xxxxxxxxx
- Date: 27 Oct 2006 04:30:58 -0700
chuchu_w@xxxxxxxxxxx wrote:
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.
Hello Hassan,
In fact, you can't... Who gave you this problem? The only way you can
do that is if the variables are bounded. Then you can turn each
variable into binary and search for a solution but still the conversion
method is not straightforward and it involves state of the art
algorithms. You can search for SAT encodings. (your problem is known as
ILP encoding into SAT and there are two well know encodings: Warners
and BBR) Try to search them up, other wise I can send you the
references for their papers.
Regards,
Paulo Matos
Thanks in advance.
Hassan
--
--------------------------------- --- -- -
Posted with NewsLeecher v3.7 Final
Web @ http://www.newsleecher.com/?usenet
------------------- ----- ---- -- -
.
- References:
- Solve math inequelity with SAT resulotion
- From: chuchu_w@xxxxxxxxxxx
- Solve math inequelity with SAT resulotion
- Prev by Date: Re: Integral works MuPAD 3.0, but not 4.0
- Next by Date: Re: An Integral to be solved or simplified
- Previous by thread: Solve math inequelity with SAT resulotion
- Next by thread: Re: Solve math inequelity with SAT resulotion
- Index(es):
Relevant Pages
|
