Pseudo-Boolean Competition 2009

The 2009 pseudo-Boolean competition is organized as a special event of the SAT 2009 conference. Like the previous evaluations (PB05, PB06, PB07), the goal 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 competition, please get in touch with


Slides of the presentation at SAT'09
See the detailed results
Booklet containing the description of solvers and instances

The next competition will be organized in 2010 (see PB10).

Here are some links to the solvers that were submitted:
Here are the archives of the instances submitted this year (see also the instances of the PB07 competition).


This year, two judges were in charge of taking the decisions that couldn't or shouldn't be taken by the organizers.
The organizers are greatly indebted to Heidi Dixon (author of the pbChaff solver) and Peter Barth (author of the opbdp solver) who have accepted this task.

The judges decided of the selection of instances (they selected all PB07 instances except the reduced ones as well as all instances submitted this year) and approved the ranking scheme.


The timetable of the 2009 evaluation is detailed below.

Opening of registration site March, 2009
Submitters must request a login on the registration site by April 1, 2009
Solvers and benchmarks submission deadline
April 26, 2009
Solvers running End of April 2009
Solvers description must be provided by May 31, 2009
Results will be given during the SAT 2009 conference June 30-July 3, 2009

Call for solvers

We encourage the submission of any kind of pseudo-Boolean solver (complete or incomplete solvers, working on linear or non-linear constraints, etc.). There are a few simple requirements to ensure that a submitted solver will correctly operate in the evaluation environment. It is expected that any pseudo-Boolean solver can be easily modified to conform to these requirements. People interested in submitting a solver can contact the organizers to get some help.

All the details about the input format, the output of the solver and its running environment are available on a separate page.

Sample code, parsers for a few languages and a few programming tips are also available.

Benchmarks to test your solvers are available from the PB07 site as well as the results of the PB07 evaluation
Some conformance tests are available.

Solver submitters implicitly accept that the results of their solver be publicly available on the evaluation web site.
Solver submitters are strongly encouraged to make their solver publicly available, either in source code or in executable format. However, this is not a requirement for entering the evaluation.

Solvers submitted by the organizers

Organizers may submit their solvers but the submitted solvers must be publicly available (either in source code or in executable format) on April 1st, 2009.

Call for benchmarks

Benchmarks may be submitted in any reasonable format. The organizers will do their best to translate the submitted benchmarks to the input format adopted for the evaluation. A benchmark submitted in the format of the evaluation will still be normalized to ensure consistency among all the input files.

We would particularly appreciate the submission of
Submitted benchmarks will be made available on the evaluation web site shortly after the beginning of the evaluation. We cannot accept benchmarks which are not publicly available (because anyone must be able to reproduce the experiments of the evaluation).

Benchmarks submitters may provide a description of their benchmarks set to be made available on the evaluation web site.

Benchmarks of the previous evalutaion can be downloaded from the PB07 site


To reach the organizers, send an email to

INESC-ID, Lisboa, Portugal
vmm at / home page
CRIL, Université d'Artois, France
olivier.roussel at / home page