[PPL-devel] Opposing inequality to equality conversion.

[Axel Simon]

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.