4

I need to prove an inequality (or find a counter example) given several assumptions (also inequalities). Unfortunately the inequality to prove is a quite long and complicated expression. There are about 15 variables and FullSimplify's output fills several A4 pages. For examples with less variables, FindInstance helps to find a counterexample or gives a result of {} if the inequality is true. I also tried to use Reduce in that way:

Reduce[
   Implies[
      assumtion1 && assumtion2,
      inequality
   ],
   Reals
]

For simple examples this outputs "True", if the inequality holds. But in my case, after several hours of running time Mathematica needed 5-6 GB of RAM (and swap) so I had to abort the process.

Is there anything that I could do with Mathematica to improve the performance?

Sjoerd C. de Vries
  • 16,122
  • 3
  • 42
  • 94
lumbric
  • 7,644
  • 7
  • 42
  • 53
  • 5
    What you do is a subset of quantifier elimination, see http://mathworld.wolfram.com/QuantifierElimination.html, and this has doubly exponential complexity in worst-case scenarios... – Per Alexandersson Dec 11 '11 at 11:40
  • What's the form of the two assumptions? – rcollyer Dec 12 '11 at 04:41
  • Well there are more than 2 assumptions. The assumptions are inequalities too and I have 32 of them to be precise. All inequalities and the ineuqality I have to prove contain 28 different variables. I suppose @Paxinum gave the correct answere already why it's just not possible to solve it in that way. I hoped there is some kind of different solution but I ran out of ideas. I'd be happy too about any inspiring hints how to continue working on it... :) Is there anything I can do to solve this problem or would it be better if I try to find a different way with less variables? – lumbric Dec 12 '11 at 12:47
  • You could try converting the implication to `!P \[Or] Q` form. I don't know if it will help, but it might. – rcollyer Dec 12 '11 at 14:34
  • Combine what I said above with `LogicalExpand` and possibly follow it with `Simplify`. At that point, you may be able to separate out your inequalities into non-overlapping subsets. Mostly, this is just a guess, but it has [worked for me in the past](http://stackoverflow.com/a/7754414/198315). – rcollyer Dec 12 '11 at 15:33
  • I managed to reduce everything to 11 variables by hand. But unfortunately also with LogicalExpand there is no way to get a result. LogicalExpand just translates everything to the form you suggested in your comment earlier. This means that basically I have a lot of inequalities with one variable (these come from the assumptions, I have bounds for most variables) and one inequality with all the variables. I don't think that there are non-overlapping subsets of inequalities. – lumbric Dec 13 '11 at 16:13
  • I think that without getting more specifics, people won't be able to help you much more. Can you supply some more details of the problem you're looking at? (If the code is really long, paste it at http://pastebin.com/ or http://gist.github.com/, etc) – Simon Dec 19 '11 at 14:23
  • This has come up several times on MathGroup, and the answer is always similar: [the algorithm that Mathematica uses has a double exponential complexity in the number of variables](https://groups.google.com/d/msg/comp.soft-sys.math.mathematica/_0GoTcUisBw/7dNScmaG0yQJ). Now I'm not familiar with the mathematics of this, but there's a good chance there will be no solution. What you absolutely must do is post a few examples of what you're working with: maybe they some some special property that will allow a different solution. But as Paxinum said: it's unlikely that `Reduce` can be sped up. – Szabolcs Dec 19 '11 at 14:53
  • Also, I think you'd have more like finding experts on the topic in either math.SE or MathOverflow. But then you probably need to rephrase your question and ask about what fast algorithms exist for solving the particular (not general) inqeualities you're dealing with. (But then again, I'm not familiar with the mathematics of this, so I might be wrong.) – Szabolcs Dec 19 '11 at 14:57
  • @lumbric It might be hard for people to answer without something to go on... would you mind linking to your notebook or showing a smaller example that makes mma hang? – abcd Dec 19 '11 at 15:27
  • Sorry i can't provide a helpful comment, but I'll just say that my experience with Mathematica improved a lot when I stuck another 8gb of memory in the computer to go with the 4gb I already have. Mathematica crashes about half as often, now... – cormullion Dec 21 '11 at 20:03
  • @cormullion Hmmm... tripling the memory only halved the crashes? Mma is much worse of a memory hog than I thought it was ;) – abcd Dec 21 '11 at 21:45
  • @yoda :) yes it's now quicker for Mathematica to return results, and so quicker for me to eventually type something stupid and crash the thing... – cormullion Dec 21 '11 at 21:58
  • What kinds of assumptions / inequalities do you have? (linear/polynomial/trigonometric/exponential/etc.) – user1071136 Dec 25 '11 at 22:08

1 Answers1

4

You will find a very nice paper on Mma CAD algorithms here

The cylindrical algebraic decomposition (CAD), which Mma uses, scales with a double exponential behavior on the number of variables.

Newer methods are double exponential in the number of quantifier alternations.

I think you'll have no luck using only the Mma internal engine, but you may roll your own based in the symmetries of your problem (if any)

Dr. belisarius
  • 60,527
  • 15
  • 115
  • 190