Pseudo Boolean Evaluation 2005

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

Registration and file upload


Pre-registration (solvers and benchmarks) March 16, 2005
Solvers Submission March 23, 2005
Benchmarks Submission March 23, 2005
Solvers running April 2005
Results June 19-23, 2005

Solver Submission

The evaluation of the solvers will be performed on a cluster of PC running under the Linux operating system. Solvers may be submitted either in source code or as a statically linked executable. If the solver requires some specific libraries or some third party software, the authors are invited to contact the organizers in order to make sure we can make them available in the evaluation environment.

Solver requirements

Requirements for solvers are quite simple. More details here.

Solver category

A solver may be able to
To assess the different solvers characteristics, there will be two evaluations: one for optimization, the other for satisfiability. A solver which is able to optimize will enter both categories. When asked about satisfiability, an environment variable PBSATISFIABILITYONLY will be set to 1 to indicate that it should stop as soon as it discovers a model.

Authors will be required to indicate if their solver can perform optimization or if it can only decide the satisfiability of the formula.

Benchmark Submission

Benchmark may be submitted in any reasonable format. Each benchmark will be translated to a common syntax to avoid any problem. See here for some details about the syntax of the generated files.


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