Pseudo Boolean Evaluation 2006

The second Pseudo Boolean evaluation is organized as a special event of the SAT 2006 conference. It follows the first Pseudo Boolean evaluation which gathered together 8 solvers. 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 pbeval@cril.univ-artois.fr.

Deadlines

The timetable of the 2006 evaluation is detailed below. Deadlines will be strict.

new

The results of the evaluation are now publicly available here. new

Opening of registration site	March 13, 2006
Pre-registration (solvers and benchmarks) expected on	April 2nd, 2006
Solvers must be submitted before	April 30, 2006
Benchmarks must be submitted before	April 30, 2006
Conformance test and bug fixes	May 1-14, 2006
Solvers running	May-June 2006
Solvers description must be provided by	June 26, 2006
Results will be given during the SAT 2006 conference	August 12-15, 2006

Noticeable changes

We report here the most important changes in the evaluation rules (in comparison to the PB'05 evaluation). As some other minor points were also modified, you are invited to read completely and carefully the call for solvers and benchmarks.

the input file format is simplified: variable names will all start by a lower 'x' followed by an integer. Solvers can therefore ignore the 'x' character and consider that variables are identified by an integer. The star character between a variable and its weight is removed. More details...
each solver is asked to output an 'o ' line each time it finds a solution with a better value of the objective function. This 'o ' line should only contain the value of the objective function (as found in the input file) for this new solution. This will enable an analysis of the way solvers progress toward the best solution. More details...
solvers are not allowed to create any file outside the directory specified by the TMPDIR environment variable. Solvers creating temporary files in /tmp or in the current directory will be rejected. More details...
a 'v ' line must be terminated by a new line character (otherwise it will be considered as truncated and ignored). More details...
only the 's ' line will be considered to determine the solver answer. The exit code of the solver will be recorded, but otherwise ignored. More details...
submitters are required to provide a description of their solver that will be available on the evaluation web site.
submitters must register their solver to the category that their program is able to solve reliably. A solver which does not solve the optimisation problem must be registered in the SAT/UNSAT category. More details...

Call for solvers

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 get in touch with 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.

A preliminary set of benchmarks is available for testing the solvers

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.

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

industrial benchmarks
benchmarks generators (written in any reasonable language)
benchmarks set with a wide distribution of their number of clauses, cardinality constraints and pseudo-Boolean constraints

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.

A preliminary set of benchmarks is available for testing the solvers

Organization

To reach the organizers, send an email to pbeval@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