Latest news

The two versions of ppfolio (sequential and parallel) did unexpectedly well at the SAT 2011 competition. ppfolio parallel got 11 medals and ppfolio sequential obtained 5 medals, which is extremely surprising. It should be recalled that ppfolio is only a system tool to run the solvers in parallel, assigning them a given set of cores. This is essentially equivalent to typing the following command line: 
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:

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:

Description of ppfolio


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
When wall clock time is the only thing that matters, the performances of ppfolio are a threshold to identify good and less good solvers. Indeed, if a parallel solver, or a portfolio doesn't perform significantly better than ppfolio, then it was probably not worth spending a lot of time developping this parallel solver or portfolio.

Submission to the SAT 2011 competition


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

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 selecting the 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.