Queries are of the form:
maximize versions P1, P2, P3, ... Pk in that order (so P1 has priority over P2
which has priority over P3 ...)
and then conditions on the versions of other packages up to n such that the 
initial working configuration  of versions is included in the
list of possible responses.

Two configurations are equal if they have the same versions for every
package.

We say that configuration 
C' = P1.v1', P2.v2', ..., Pk.vk', ..., Pn.vn'
is lexicographically greater (>) than
C = P1.v1, P2.v2, ...., Pk.vk, ..., Pn.vn

if either P1.v1' > P1.v1
or (P1.v1' = P1.v1 and P2.v2' > P2.v2)
or ...
or (P1.v1' = P1.v1 and P2.v2' = P2.v2 and ... and Pk-1.vk-1' = Pk-1.vk-1
and Pk.vk' > Pk.vk)

We say that a configuration C' is between C and C''
if C <= C' <= C''.

A configuration "works" if it executes to completion. 

Assumptions: 


1. Historicity:
Suppose vi < vi' < vi'', vj < vj' < vj'',  and that Pi.vi' works with Pj.vj'
but Pi.vi'' does not work with Pj.vj'.
Then (i) Pi.vi'' will not work with Pj.vj
and (ii) if vi''' > vi'', then Pi.vi''' will not work with Pj.vj'.


Algorithm: LiquidClimber

This starts from a configuration that works (e.g. the one that 
was run by the original creators of the virtual machine).
It assumes that there is some query that maximizes the versions
of some packages (perhaps with constraints) and may have constraints
but no maximization function on other versions.

current := package version pairs in the initial configuration
todolist := packages requiring maximization in descending order of priority
done := packages already taken care of (will be top priority ones)
while todolist is not empty
   p := first element of todolist
   move p to done
   keepwork := True
   while keepwork
      update current to the highest version of p that works (use git binary)
      if current has last version of p then
          keepwork := False
      else
	versionstodo = find all greater versions of p or major releases 
		in ascending order of version number
	for each v in versionstodo
	  if keepwork
        	temp := current with p set to v
		ret := trytomakework(temp)
		if ret is not null then
			current := ret
		else
			keepwork:= False 
			# No higher version will work by historicity
	keepwork:= False
	


# adjust
trytomakework(temp)
	while temp doesn't work
	  in the execution of temp,
	    find the first other package p' that 
	    	causes the execution to fail
	    perform binary search on higher versions of p' 
		that satisfy the query constraints
	    	to find the least version v of p' such that
	    	using p'.v in temp causes the execution to go
	    	past the point where it crashed before
	    if no such v then
		return null
	    else 
		update temp with p'.v
	endwhile
	return temp
         
Why should this work?

Theorem: Under the assumption of historicity, 
the value of current at the end of this algorithm is the lexicographically
maximum.

Proof sketch:
Suppose that this algorithm arrives at a lexicographically maximum
configuration of 
P1.v1', P2.v2', ...., Pn.vn'
that works.
Suppose that there is a another configuration 
P1.v1'', P2.v2'', ...., Pn.vn''
that is lexicographically greater and that also works.
We prove that 
P1.v1'', P2.v2'', ...., Pn.vn''
must have been tried by our algorithm..

If v1'' > v1' then the algorithm must have tried v1'' by construction of
versionstodo.
When trying
P1.v1'', P2.v2', ...., Pn.vn',
let j be the package that first fails.
Then Pj.vj'' != Pj.vj', or there would not have been
a failure since C'' works. Further Pj.vj'' > Pj.vj'  by historicity. 
So, some version of Pj, vj''' will be found that allows the execution
to pass that call to Pj.
As the iterations through trytomakework continue
the version of Pj may or may not continue to increase.
If Pj is one of the packages whose version should be maximized, then
if vj'' > vj''', then vj'' will be tried by construction of versionstodo.

Inductive step: this is true up to m-1 for 1 < m-1 < k-1, then
it will be true for m.

If vm'' > vm', then when trying
P1.v1'', P2.v2'', ..., Pm.vm'', ...., Pn.vn',
let j be the package that first fails.
<Then same argument as above.>