[SMT-COMP] Results

[Martin Nyx Brain]

On Mon, 2019-07-08 at 14:09 +0200, Tjark Weber wrote:
> On Sun, 2019-07-07 at 14:43 -0700, Aina Niemetz wrote:
> > the results of SMT-COMP 2019 are available at
> > https://smt-comp.github.io/2019/results.html
> 
> With the 2019 competition results available, now might be a good time
> to think about portfolio solvers (aka wrapper tools). These have been
> allowed in the competition for a long time but no portfolio solvers
> were actually submitted in recent years.
> 
> This year, I submitted a simple portfolio solver (Par4) that
> performed
> rather well in many of the divisions into which it was entered. I
> probably spent far less time on this solver than the developers of
> the
> wrapped tools spent on their solvers. Credit to them! If people start
> developing portfolio solvers in earnest, it might become difficult in
> the future to win any division with anything but a portfolio
> approach.

Given you are pitting a selection algorithm and the VBS of last year's
competition against a year's worth of improvements in a single solver,
in some ways, it is a massive endorsement of the hard work of various
solver developers when a portfolio solver *doesn't* win.

> There are different options for how portfolio solvers could be
> treated
> in future competitions: run them like any other solver; rank them
> separately from ordinary solvers; run them hors concours; or do not
> allow them at all. Perhaps we should have a discussion to identify
> which of these options would be most beneficial to the competition
> and
> to progress in SMT solving in general.

I think it rather depends on what the objectives / purpose of the SMT
competition is.  If it is to find / show-case the best solver then ..
portfolio solvers are often the best.  If it is to support / reward /
encourage / chart / record improvements in solver techniques then it
seems like maybe they should be separated from "single system" solvers.

As I'm giving unhelpful answers, maybe I will continue to do so... what
 defines a portfolio solver?  Would a portfolio of instances of the
same solver but run with different configurations count?  What happens
if that is done within the solver as some of the parallel SAT solvers
do?

Cheers,
 - Martin