Pseudo Boolean Evaluation 2005

The 2006 pseudo-Boolean evaluation is organized as a special event of the SAT 2006 conference. See the PB'06 web page for the deadlines and new rules.

The Pseudo Boolean evaluation is organized as a special track of the SAT COMPETITION 2005. The goal of this evaluation is to assess the state of the art in the field of Pseudo Boolean solvers.

For questions, comments and any other issue regarding the PB Evaluation, please get in touch with pb05@cril.univ-artois.fr.

Results of the evaluation

The evaluation was performed in two steps. The first phase which took place from April to June 2005 allowed to run several versions of the solvers and to detect the first bugs in the solvers implementation. Unfortunately, the bug correctives that were submitted by the authors still had some bugs. Therefore, the results that were presented to the SAT conference in June 2005 were not completely satisfying since every solver had at least a problem (but some of these problems where simple mistakes in the solvers output).

To obtain more reliable results, it was decided to run the solvers one last time in September. Authors were allowed to fix the bugs as well as to improve their solver. During this second phase, only one version of the solvers was allowed to run.

See here for the results of the second phase of the evaluation.
See here for the results of the first phase of the evaluation. As most of the solvers had some problems in this first phase, these results are of little interest now. They are merely archived.

Keep in mind that this event was an evaluation instead of a competition. Our goal was to take a snapshot of the current state of the art rather than to obtain a ranking of the different solvers (because we couldn't get it right on our first try).

Submitted solvers

Eight solvers (with several variants or versions) were submitted to the evaluation

Solver	Authors	Link
bsolo	Vasco Manquinho and João Marques-Silva
galena	Donald Chai and Andreas Kuehlmann
minisat+	Niklas Eén and Niklas Sörensson
PBS4	Fadi Aloul and Bashar Al-Rawi
pb2sat+zchaff	Olivier Bailleux, Yacine Boufkhad, Olivier Roussel
Pueblo	Hossein Sheini and Karem Sakallah
sat4jpseudo	Daniel Le Berre, Mederic Baron, Anne Parrain, Olivier Roussel
vallst_0.9.258	Daniel Vallstrom

Other material

Benchmarks used during the evaluation are available here.
The call for solvers and benchmarks is archived here.

Acknowledgement

The authors are greatly indebted to Daniel Le Berre and Laurent Simon for providing the scripts of the SAT competition, to the LINC Lab, Department of ECECS, University of Cincinnati for providing the computing resources and to Robert Montjoy for his assistance. Special thanks to Michal Kouril for his great help and his continuous interest in this evaluation.

Next evaluation

The second pseudo-Boolean evaluation is organized as a special event of the SAT 2006 conference.

See the PB'06 web page for the deadlines and new rules.

Organization

To reach the organizers, send an email to pb05@cril.univ-artois.fr.

Vasco MANQUINHO
INESC-ID, Lisboa, Portugal
vmm at sat.inesc.pt / home page

Olivier ROUSSEL
CRIL, Université d'Artois, France
olivier.roussel at cril.univ-artois.fr / home page