[PPL-devel] SICStus interface and backtrack

[Tristan Denmat]

Dear Pat,
Thank you very much for your answers. I don't know yet if it will solve 
my problems but I will try. I like the way you do the backtracking, that 
is clever. 
I can say a few words about what I am doing.
I am using constraint solving to do program properties verification 
(actually you have seen my talk at WLPE this year).
The basic idea is to translate the problem of finding a counter example 
to property into a constraint solving problem.
A solution of the constraint problem is an execution that violates the 
given property. If there is no solution to this problem, the program 
satisfies the property.

We are using clp(fd) to do that. The problem is that doing propagation 
on our constraint system gives results similar to the analysis of the 
program on the intervals abstract domain.  Consequently, if the 
properties we want to refute is relational, the propagation is almost 
never able to detect inconsistencies in the constraint system.  In this 
case, we need to enumerate all the values of potentially very large 
domains before knowing that there is no solution.

As you suggested in Barcelona, using a symbolic solver can help. In 
fact, that is what I am doing now : making clp(fd) and the PPL 
communicate to take advantage of both of them. CLP(fd) allow us to 
define global constraints that are far from linear. PPL allow us to 
detect inconsistencies in the linear relaxation of the clp(fd) 
constraint store.
A very simple example is the constraint store: X = Y + Z, X < Y + Z.
CLP(fd) doesn't detect inconsistency whitout labeling whereas this is 
trivial for the PPL.

I don't think that I am very clear. Let me know if you want more details...

Regards,
Tristan Denmat

IRISA - Rennes
France




> Dear Tristan,
>
> You are describing a problem with any interface between a declarative 
> language and an imperative language. That is that the backtracking 
> over the interface needs special attention that is likely to lose 
> efficiency.
>
> As I understand what you are saying, at the moment, you are only using 
> the PPL to update the constraint system L to L' and it is the 
> attributed variables that are the main data objects here.
>
> Obviously, I do not know exactly your particular application and 
> problem but if you wish to use the PPL to do all the work and use the 
> handlers instead of the attributed variables, then you can - but you 
> do need to be careful with the backtracking. If you have a PPL 
> polyhedron and just want to add a constraint which is removed on 
> backtracking, it may be best to copy the polyhedron and work on the copy.
>
> This approach is taken in some of the examples used to test the Prolog 
> interface. That is, a copy of the polyhedron is made before adding a 
> constraint (and work on the copy). To make sure that this copy is 
> deleted on backtracking, extra code is added for backtracking. For 
> instance, in ppl/interfaces/Prolog/tests/clpq2.pl we have:
>
>   [...],
>   % Copy the current polyhedron and work on the copy.
>   ppl_new_NNC_Polyhedron_from_NNC_Polyhedron(Poly, Poly_Copy),
>   % On backtracking, clean up the unwanted polyhedron
>   cleanup(Poly_Copy),
>   [...],
>   ppl_Polyhedron_add_constraints_and_minimize(Poly_Copy,
>                                                  Binding_Constraints),
>   [...].
>
>
> with cleanup/1 defined as
>
> % To prevent leaks:
> % First succeed and then, on backtracking,
> % remove the unwanted polyhedron before failing.
> cleanup(_Polyhedron).
> cleanup(Polyhedron) :-
>   ppl_delete_Polyhedron(Polyhedron),
>   fail.
>
> The same idea is used in ppl/interfaces/Prolog/tests/cpl_check.pl to 
> delete polyhedra after unexpected failure causing backtracking.
>
> If you then want to work on the original polyhedron, you could use PPL 
> intersection between the original and copied polyhedron.
> Note though that once you do this, you can no longer undo things by 
> backtracking.
>
> The other way of course is to avoid backtracking altogether....
>
> BTW I see you are using version 0.7. Note that version 0.9 of the PPL 
> has been released on March 12th. Apart from complete support for 
> rational grids (i.e., solutions of finite systems of congruence 
> relations like x + y - 2*z = 3 (mod 6), it includes also many 
> portability improvement and a couple of bug fixes. (Note that, in this 
> release, the Grid class does not yet have a Prolog interface.) 
> Although you will need to make some minor changes to your code (for 
> instance, names of some PPL predicates have been changed), version 0.9 
> is an improved system, so do use it if you can (and do please let us 
> know of any problems you have if you cannot).
>
> Can you tell us more about your application?
>
> Best wishes,
>   Pat
>
> Dr Pat Hill
> School of Computing
> University of Leeds
>
> On Thu, 16 Mar 2006, Tristan Denmat wrote:
>
>> Dear all,
>> I am currently using the PPL (version 0.7) with SICStus.  Everything 
>> was fine until I met important efficiency issues...
>>
>> The problem is (or might be) that I want my program to be 
>> backtrackable. I mean, if I add a constraint to a polyhedra, I want 
>> this constraint to be removed when Prolog backtracks before the 
>> addition.
>> As far as I know, it is not possible to do so if I directly use the 
>> handlers.
>> To adress that I represent a polyhedron by an attributed variable P 
>> containing the list of constraints that define it (say L). Then, when 
>> I want to add a constraint (C) , I create a new Polyhedron from L in 
>> ppl, add C, get the minimized list of constraints (L'), delete the 
>> Polyhedron and update my variable P to L'.  If Prolog backtracks 
>> before the addition, the old value L of P is automatically restored. 
>> I am afraid that this implementation is dramatic for the efficiency 
>> of your library.
>>
>> My questions are :
>> Do you already have tackled the problem of backtrack with PPL ? If 
>> yes, would you have a better solution than mine ?
>> How bad is this approach regarding efficiency ?
>> Would it make sense to save a kind of "internal state" of the 
>> polyhedron instead of the explicit list of constraints ?
>