Invariants and cycles

From CometPublic

[edit] Invariants

The architecture of COMET consists of a declarative and a search component organized in three layers.

Image:Architecture.png

The first layer is the concept of invariants over algebraic and set expressions.

An invariant is a declarative component specifying a relation to be maintained incrementally, not how to update it:

An invariant is an one-way constraint (see Sketchpad and ThingLab) expressed in terms of incremental variables which specifies a relation which must be maintained under assignments of new values to its variables.

In COMET, an invariant is an instruction of the form

v <- exp;

where v is an incremental variable. COMET guarantees that, at any time during the computation, the value of variable v is the value of the expression exp.

Here is a little example of use of invariants:

include "LocalSolver";

// Declares the model
LocalSolver m();

// Declares the variables
var{int} a(m);
var{int} b(m);
var{int} c(m);

// Declares the invariant
b <- c + a;
c <- a;

// Closes the model
m.close();

// Assigns a (Comet propagates the values)
a := 3;

cout << "a=" << a << endl;
cout << "b=" << b << endl;
cout << "c=" << c << endl;

// Re-assigns a (Comet propagates the new values)
a := 4;

cout << "a=" << a << endl;
cout << "b=" << b << endl;
cout << "c=" << c << endl;

The ouput will be:

a=3
b=6
c=3
a=4
b=8
c=4

Note that incremental variables used as left side of invariants cannot be used as left side of assignments. Any attempt to assign directly such a variable will raise the error

Localizer Error: You cannot assign a variable which is already bound to an invariant

For example, the code

include "LocalSolver";

LocalSolver m();

var{int} a(m);
var{int} b(m); 

// Declares the invariant
a <- b;

m.close();

// Assigns b (Comet propagates the value)
b := 3;

cout << "a=" << a << endl;
cout << "b=" << b << endl;

// Assigns a (Comet raises an error)
a := 2;

cout << "a=" << a << endl;
cout << "b=" << b << endl;

will give the output

a=3
b=3
ici
Localizer Error: You cannot assign a variable which is already bound to an invariant

COMET includes

• numerical invariants
• set invariants
• combinatorial invariants

[edit] Static invariants and cycles

Static invariants are invariants where dependences between their variables are explicit, i.e. can be accurately determined at compile time, e.g.

x <- y * z;

For such invariants, it is simple to find a partial ordering that guarantees that each pair <variable,invariant> is considered at most once. As mentioned in Constraint-Based Local Search

This [The existence of a partial ordering for static invariants] assumes there are no cycles in the depency graph, which is the case in combinatorial optimization applications

Oddly, given the dependency graph

Image:Static cycle.png

associated to the code above, COMET does not detect the static cycle.

include "LocalSolver";

LocalSolver m();

var{int} a(m);
var{int} b(m);
var{int} c(m);

// Declares two invariants with a static cycle involving the variables b and c.
b <- c + a;
c <- b + a;
m.close();

// Assigns a (Comet does not detect the cycle, propagates the values and eventually
// produces a result which is not consistent with the invariants)
a := 3;

cout << "a=" << a << endl;
cout << "b=" << b << endl;
cout << "c=" << c << endl;

Indeed, the ouput will be

a=3
b=3
c=6

i.e. COMET consider in turn the first and the second invariants and the produce inconsistent values.

[edit] Dynamic cycles

Dynamic invariants are invariants where dependences between their variables are not known accurately when a model is closed, i.e. where dependences can only be resolved at run time. For example,

start[i] <- start[prec[i]] + duration[prec[i]]

For such invariants, the dependency graph seems to have cycles, although, at run time, none of these cycles actually materializes. COMET will

• decompose the dependency graph in strongly connected components (S.C.C.)
• compute once a S.C.C. priority ordering to propagate the invariants

so that when a S.C.C. is considered, the values of all the invariants in previous S.C.C. have been updated. The pseudocode taken from Constraint-Based Local Search is

procedure execute(I)
begin
  <I0,..,Ip> := serialize(I);
  for(i := 0;i <= p;i++) do
    t := plan(Ii);
    execute(Ii,t);
  endfor;
end

When the model is closed, there are:

• a planning phase
  • invariants are normalized into primitive invariants
  • a suitable order to propagate the changes is determined
• propagation
  • propagation are carried out

For example, consider the code

include "LocalSolver";
	
LocalSolver m();

var{int} i(m);
var{int} a[0..1](m);
var{int} b[0..1](m);

//Assigns a[0] and a[1]
a[0] := 42;
a[1] := 24;

// Declares the dynamic invariant.
b[0] <- a[i];
b[1] <- a[1-i];
m.close();
	
// Assigns i (Comet finds the effective dependences)
i := 1;
	
cout << "i=" << i << endl;
cout << "a=" << a << endl;
cout << "b=" << b << endl;

We get the potential dependency graph

Image:Ex1 compile time graph.png

will simplify at runtime in the effective dependency graph

Image:Ex1 run time graph.png

and the ouptut is

i=1
a=a[42,24]
b=b[24,42]

Here is another code which contains a SCC:

include "LocalSolver";

LocalSolver m();

var{int} i(m);
var{int} a[0..2](m);

a[0] := 42;

// Declares the invariants (Comet notices a SCC)
a[1] <- 1+a[2*i];
a[2] <- 2*a[1-i];
m.close();

// Assigns i (Comet finds the effective dependences)
i := 0;

cout << "i=" << i << endl;
cout << "a=" << a << endl;

The potential dependency graph is

Image:Ex2 compile time graph.png

whereas the effective dependency graph is

Image:Ex2 run time graph.png

We get the output

SCC[0] = strongly CC (3,6,2)[0]
i=0
a=a[42,43,86]

Note that COMET tells us that it has noticed the SCC.