On Feb 6, 2009, at 12:34, Roberto Bagnara wrote:
Hello Axel.
Axel Simon wrote:
I'm trying to verify a claim in Halbwachs' paper on factoring polyhedra ("Some ways to reduce the space dimension in polyhedra computations" is the journal version). Specifically, he claims that omitting a common equality relation from the convex hull computation yields not significant speedup. I've tried to run a convex hull calculation, once with the common equalities added and once with the common equalities omitted and found quite a difference in performance.
The difference is in favor of which technique? (This is probably implicit in what you write afterward, but I would like to be sure.)
Sorry, I don't think I was as clear as I could have been. I'll try again:
It's about calculating the convex hull using the double-description method in PPL. Suppose you have two polyhedra described by the inequality sets I_1 and I_2. Let x be a variable not occurring in I_1 nor I_2 and x=le an equality where le denotes a linear expression over the variables in I_1 and I_2. He claims that:
calc_hull(I_1, I_2)
is not significantly faster than calculating
calc_hull(I_1 \cup { x=le }, I_2 \cup { x=le }).
This is what I'm trying to verify. However I'm adding the equality x=le as two opposing inequalities x<=le and x>=le to the constraint systems I_1 and I_2 before running PPL's convex hull operation.
However, I added the equality as two opposing inequalities. My question: are the two opposing inequalities not immediately turned into one equality by the Constraint class? If not, then this might explain the speed difference I'm seeing.
If I understand correctly, you are asking whether the Constraint_System class immediately turns two opposing inequalities into the corresponding equality. The answer is negative. This kind of simplification only happens (lazily) as part of the conversion/minimization process.
Ok, that is interesting. So I might observe a different performance if I add the equality as x=le rather than as two opposing inequalities.
Thanks, Axel.