Cylindrical Algebraic Decomposition

Help
2014-03-16
2015-10-30
  • Aristotelis

    Aristotelis - 2014-03-16

    Hello,

    I am new to REDUCE. I am trying to perform Cylindrical Algebraic Decomposition on a set of inequalities but I am completely unfamiliar with the syntax, and I cannot find any examples. In mathematica, I use:

    CONS=
    A1 > 1/10 && A1 < 50 &&
    A2 > 1/10 && A2 < 50 &&
    A3 > 1/10 && A3 < 50 &&
    A4 > 1/10 && A4 < 50 &&
    -(33/A1) - (139/2 + Sqrt[2])/A2 - 6/A3 - (14 Sqrt[2])/A4 >= -6

    CylindricalDecomposition[CONS, {A1, A2, A3, A4}]

    I get:

    -(3300/(-449 + 30 Sqrt[2])) < A1 < 50 &&
    (-3475 A1 - 50 Sqrt[2] A1)/( 1650 - 294 A1 + 14 Sqrt[2] A1) < A2 < 50 &&
    -((300 A1 A2)/( 3475 A1 + 50 Sqrt[2] A1 + 1650 A2 - 300 A1 A2 + 14 Sqrt[2] A1 A2)) < A3 < 50 &&
    (28 Sqrt[2] A1 A2 A3)/(-12 A1 A2 - 139 A1 A3 - 2 Sqrt[2] A1 A3 - 66 A2 A3 + 12 A1 A2 A3) <= A4 < 50

    Is it possible to set up this problem with REDUCE?

    TIA,
    Aristotelis

     
  • Robert Pollak

    Robert Pollak - 2015-10-30

    Hello Aristotelis,

    have you found out? I would also be interested.

    -- Robert

     
  • Thomas Sturm

    Thomas Sturm - 2015-10-30

    Redlog (www.redlog.eu), which is part of Reduce implements CAD and various other real quantifier elimination methods. I do not quite understand what your objective is exactly, because In your example you do not quantify any variables.

    For your example you would in principle start as follows:

    rlset r;  % load Redlog and set the domain to real numbers
    
    on rlposden;  % allow variables in denominators assuming that they are positive
    
    phi := A1 > 1/10 and A1 < 50 and
       A2 > 1/10 and A2 < 50 and
       A3 > 1/10 and A3 < 50 and
       A4 > 1/10 and A4 < 50 and
       -(33/A1) - (139/2 + sqrt2)/A2 - 6/A3 - (14 sqrt2)/A4 >= -6;
    
    psi := sqrt2 >= 0 and sqrt2^2=2;
    

    Note that sqrt2 is just another variable here, and psi can be used to define it in the context of quantifier elimination. For example:

    rlqe ex({sqrt2, a4}, phi and psi);

    yields neccessary and sufficient conditions in a1, ..., a3 for the existence of an a4 in your example. You can explicitly call rlcad instead of rlqe to force the use of CAD, but it is better to let Redlog decide what is best.

    You find more details on the Redlog website mentioned above.

    Best,

    Thomas

     

Log in to post a comment.

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks