solver1 & solver2 & solver3 & solver4 & solver5 &Therefore, the results obtained by this portfolio are only due to the base solvers selected, which are the actual solvers to deserve a medal. Here are the medals that ppfolio owes to the individual solvers:

- clasp (Martin Gebser, Benjamin Kaufmann, and Torsten Schaub):
- cryptominisat (Mate Soos):
- lingeling/plingeling (Armin Biere):
- march_hi (Marijn Heule and Hans Van Maaren):
- TNM (Wanxia Wei and Chu Min Li):

It's important to emphasize that, since ppfolio is running plingeling on all but 4 cores, plingeling is essentially competing with itself in the 32 cores track.

Some of the lessons we learn from these results are the following:

- local search solvers are very effective on a significant subset of the CRAFTED benchmarks
- despite memory contention, running different solvers on each core can still be efficient
- even running solvers in sequence can be efficient
- a simple approximation of the VBS gives good results

ppfolio (Pico PortFOLIO or also Parallel PortFOLIO) is a very naive parallel portfolio. It is meant to identify a lower bound of what can be achieved either with portfolios, or with parallel solvers.

The goal of ppfolio is to offer an implementation of the Virtual Best Solver (VBS) that can run on a single host. If you have unlimited computing resources, and just want to solve a SAT instance as fast as possible (in wall clock time), your best option is to run each available SAT solver on its own computer in parallel. When a solver answers, the other solvers are killed. By definition, this VBS is at least as powerful as each individual solver (and in practice it is significantly better than each individual solver). If you have enough computers to run each available SAT solver, the VBS represents the best that can be done with the current SAT technology. All is needed to reach this optimum is to have as many computers as you have available SAT solvers. This is not so difficult, but not so common either.

However, nowadays, it is very common to have a desktop computer with 8 logical processors (4 cores with hyperthreading) and computers with 8 actual cores are not very expensive either. Therefore, it is very tempting to run a solver on each available logical processor. This is exactly what ppfolio does. It's just an approximation of the VBS that runs on a single host.

ppfolio by itself is just a program that starts SAT solvers in parallel. It only involves system programming and knows nothing about the SAT problem. The number of cores that may be used can be selected on the command line.

ppfolio does not try to be clever in any way. Its role is just to run solvers in parallel. Several obvious improvements are possible (detecting the type of SAT instance and choosing the appropriate solver, improving the scheduling of the solvers, sharing of the formula,...) but were not considered because the goal of this solver is uniquely to identify a lower bound on the performances that can be achieved using a few lines of plain system programming. It is of course expected that access to main memory will be a bottleneck that will significantly impact each individual solver performances.

It is important to emphasize that ppfolio

- is not actually a SAT solver. It's only a tool to run SAT solvers concurrently
- is not green. It wastes a lot of CPU resources because the different solvers perform redundant computations
- is not clever at all

- A 2 pages description of ppfolio (PDF file) and its source (LaTeX file) (md5sum of the LaTeX file: a12e32960624463bb1934039fff35cbf)
- Sources of ppfolio (version submitted at the SAT competition)
- Sources of ppfolio, with a GPL v3 header on ppfolio.cc (included solvers have their own license)
- Binary used during the competition

The version submitted to the SAT 2011 competition uses the following solvers:

- cryptominisat (Mate Soos)
- lingeling/plingeling (Armin Biere)
- clasp (Martin Gebser, Benjamin Kaufmann, and Torsten Schaub)
- TNM (Wanxia Wei and Chu Min Li)
- march_hi (Marijn Heule and Hans Van Maaren)

These solvers have been chosen on the basis of their results on the 2009 competition benchmark. In each category (application, crafted, random), the best solver was selected. A second solver was also selected if it could solve at least ten instances that the first solver didn't.

An easy way to improve the version of ppfolio submitted to the competition would have been to submit 3 versions of ppfolio, each one being specialized for a given category (APPLICATION, CRAFTED, RANDOM). This is trivially done by sele#tingthd top solvers in each target category. Although this is commonly done by some solvers (especially portfolios despite the fact they are supposed to be able to recognize the instance features), this was not done for ppfolio because it was judged more interesting to see what one single version can achieve in each category.

The two versions of ppfolio submitted to the competition are a parallel one (par) and a sequentiel one (seq). The parallel version uses each available core. If there's more than 5 cores available, the parallel solver plingeling is started on the remaining cores. The sequential version uses only 1 core, which implies that CPU time will be almost equal to wall clock time. Only three solvers are started in this version. The task of granting CPU usage to one solver is left to the system process scheduler. This means that each solver will run for 1/3 of the time allocated to the portfolio. Obviously, this is not the normal use of ppfolio and we can't expect good performances from this sequential version but this doesn't matter since it is only meant to identify a lower bound for other solvers.