Question about monolithic solver algorithm

[yugr]

The monolithic solver performs an exhaustive search of solutions in

  bool found_solution = false;
  while (GlobalModel* nextm = e.next()) {
    found_solution = true;
    GlobalModel * oldm = m;
    m = nextm;
    delete oldm;
  }

and reports optimal solution only if the loop managed to terminate without timeout:

  if (monolithicStop->stop(e.statistics(), ro))
    r = found_solution ? SOME_SOLUTION : LIMIT;
  else
    r = found_solution ? OPTIMAL_SOLUTION : UNSATISFIABLE;

The calling code in solver.cpp treats only OPTIMAL_SOLUTION case as successful.

Why is SOME_SOLUTION case ignored? It seems it would contain a valid (and optimal) solution as well.

[robcasloz]

Good question. The structure of the monolithic solver's search strategy, where the first found solution (if any is found at all) is guaranteed to be the optimal one, makes it impossible to end up with the SOME_SOLUTION case. See https://github.com/unison-code/unison/blob/9f9857e742156b51e6314488f4173cd1b42c4aec/src/solvers/gecode/models/globalmodel.cpp#L693-L716

As an example, this is the search tree of the monolithic solver for the Unison manual's running example (generated with uni run doc/code/factorial.mir --solverflag=--disable-presolving --solverflag=--global-budget=0 --solverflag=--local-limit=0 --solverflag=--final-aggressiveness=0 --solverflag=--gist-global --goal=speed):

Note how the first branching decision is to fix the cost to 186 (the minimum value in the cost variable domain), which makes the found solution (orange diamond) the optimal one. If the solver had found no solution with cost 186, the next branching step would have been to try out the next value in the cost variable domain, and so on until either an (optimal) solution is found, a time out occurs, or the search space is exhausted:

So the logic to handle time out solutions and the while loop structure you list above seem like an unnecessary (but harmless) result of copy-pasting code from some other part of the solver (perhaps from https://github.com/unison-code/unison/blob/9f9857e742156b51e6314488f4173cd1b42c4aec/src/solvers/gecode/procedures/localprocedures.cpp#L105-L122 or similar).

Patches welcome ;)

[bodavid]

Hi

In the case of compiling combinatorially for a specific register based CPU architecture with an intermediate virtual stack machine (in this case WebAssembly), is it possible to make any assumptions to make the utilization of CPU-registers and pipelines more efficient? I can imagine that stack machines optimize in a sense that makes this possible. Is it possible or necessary for the compilation of WebAssembly to do anything special to improve the throughput speed?

David

Message ID: @.***>