Pseudo-Boolean Competition 2012

The 2012 pseudo-Boolean competition is organized as a special event of the SAT 2012 conference. Like the previous evaluations and competitions(PB05, PB06, PB07, PB09, PB10, PB11), the goal is to assess the state of the art in the field of pseudo-Boolean solvers.

This edition of the competition will be very similar to the PB11 competition (no new problem introduced). We especially encourage the submission of new solvers and new instances.

This is the last PB competition organized by V. Manquinho and O. Roussel. Anyone interested in organizing the future PB competitions can get in touch with the organizers.

For questions, comments and any other issue regarding the PB competition, please get in touch with

Results of the competition


The timetable of the 2012 evaluation is detailed below.

Opening of registration site March 5, 2012
Submitters must request a login on the registration site by March 19, 2012
April 13, 2012
Solvers and benchmarks submission deadline
March 26, 2012
April 20, 2012
Solvers running April 2012
Solvers description must be provided by May 14, 2012
Results will be given during the SAT 2012 conference June 17-June 20, 2012

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 in this PDF file.

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

Benchmarks to test your solvers (as well as the results of the competitions) are available from the PB11 site

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 must publish on March 19, 2012 April 2, 2012 either a precise description of their solver, or the source code, or the binary of their solver, or a fingerprint of one of these.

Here are the fingerprints of the submitted solvers:

7c791e3c556b48800a1abe8f0f78bb6b  bsolo
1b5dfe1e702a32048cda9fd20e0af8ea  pwbo2.0
f2f9041f380e94b89a12d43d16fdb850  wbo1.7

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 competitions can be downloaded from the PB11 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