\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{times}
\title{Description of ppfolio}
\author{Olivier Roussel
\\
CRIL - CNRS UMR 8188\\
rue de l'Université, SP 16,
62 307 Lens Cedex, France\\
olivier.roussel@cril.univ-artois.fr}
\date{}
\begin{document}
\maketitle
ppfolio (Pico Portfolio or also Parallel Portfolio) is a naive parallel
portfolio. It is meant to identify a lower bound of what can be
achieved either with portfolios, or with parallel solvers.
ppfolio by itself is just a program that starts SAT solvers in
parallel. It only involves system programmation 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 of the performances that can be
achieved using a few lines of plain system programmation. It is of
course expected that access to main memory will be a bottleneck that
will significantly impact each individual solver performances.
The submitted version uses the following solvers
\begin{itemize}
\item cryptominisat (Mate Soos)
\item lingeling/plingeling (Armin Biere)
\item clasp (Martin Gebser, Benjamin Kaufmann, and Torsten Schaub)
\item TNM (Wanxia Wei and Chu Min Li)
\item march\_hi (Marijn Heule and Hans Van Maaren)
\end{itemize}
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 than the first
solver didn't.
The solvers that are started depend on the number of allocated cores~:
\begin{itemize}
\item[1 core:] cryptominisat, clasp and TNM are started, but since
there is only one core, the solver is essentially sequential.
\item[2 cores:] cryptominisat and lingeling are started on the first
core, clasp and TNM on the second core
\item[3 cores:] cryptominisat and lingeling are started on on their own
core, clasp and TNM on the last core
\item[4 cores:] cryptominisat, lingeling and clasp are started on their
own core. TNM and march\_hi are run on the remaining core.
\item[5 cores:] cryptominisat, lingeling, clasp, TNM and march\_hi are
started on their own core.
\item[$>$5 cores:] cryptominisat, clasp, TNM and march\_hi are started on
their own core. plingeling is run on the remaining cores.
\end{itemize}
\end{document}