2
$\begingroup$

A portfolio of solvers is a collection of solvers with different configurations that share CPU time, CPU cores, and memory resources and try to get an answer as soon as possible. Solvers might also communicate with each other. 1 The task of solver portfolio design involves computing metrics about the problem (which also takes compute time) and choosing which solvers to run for how long with how many cores based on any information you can collect about the problem (including information from solvers which already ran).

Portfolios are often more successful in SAT competitions than any single solvers 2. I am interested in literature on designing portfolios for optimization algorithms. I have been unable to find any as many searches are overshadowed by "portfolio optimization problems".

In particular, I am looking for:

  • Introductory Literature on Portfolios for Satisfiability and Optimization
  • Automation of portfolio creation based on (automated) experiments for Optimization
  • Improving any-time performance with solver portfolios
  • The trade-off between good anytime performance and good performance stopping at a certain time point
  • Automatic solver configuration exploration as the configuration space can be huge

1 See HordeSat

2 See Table 5 of SatZilla

Improve this question
$\endgroup$
5
  • $\begingroup$ If you are interested in theoretical work for this problem, I recommend the following thesis of Matt Streeter thesis . $\endgroup$
    – batwing
    Commented May 21, 2021 at 0:29
  • $\begingroup$ Thanks but the links away from this website are dead and both the links for the presentation and thesis redirect to the authors web page which doesn't contain them. Is there a way to get them without bothering the author you are aware of? $\endgroup$
    – worldsmithhelper
    Commented May 21, 2021 at 0:33
  • $\begingroup$ I am unable to find a working link, but you should be able to find the published conference papers associated with his thesis here. $\endgroup$
    – batwing
    Commented May 21, 2021 at 0:44
  • $\begingroup$ Selecting a portfolio of SAT solvers is one of the topics of this talk: youtube.com/watch?v=rEyCwoD-RwI (towards the 2nd half IIRC). You'll probably find some references from there and the speaker's webpage / publications. $\endgroup$
    – mtanneau
    Commented May 21, 2021 at 12:31
  • $\begingroup$ This talk inspired my question. It's a good resource that also mentions HordeSAT $\endgroup$
    – worldsmithhelper
    Commented May 21, 2021 at 19:54

2 Answers 2

Reset to default
3
$\begingroup$

For the automatic solver configuration, I know of this reference (there may be a journal version): A learning-based mathematical programming formulation for the automatic configuration of optimization solvers.

They also cite further references on the topic.

Improve this answer
$\endgroup$
1
$\begingroup$

I'm not sure if this is exactly on point, but there is a paper by Carvajal et al. on the use of parallel trees (with communication between them) for solving integer programs. You might also be interested in reference [10] in their paper (Koch et al.), which discusses "racing ramp-up", a technique adopted by CPLEX a while back, in which you initially turn different solver configurations loose and, after some amount of time or iterations, pick the one that seems to be making the best progress.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.