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 pb05@cril.univ-artois.fr.

Registration and file upload

Register now your solver or benchmark on our registration page.
Registered users may now upload their solver or benchmark on our upload page.

Deadlines

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

only decide if a pseudo boolean formula is satisfiable or not (SATISFIABILITY category)
find a assignment of variables which minimizes a utility function (OPTIMIZATION category)

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.

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