Pseudo Boolean Evaluation 2005
2006 pseudo-Boolean evaluation is organized as a special event of
the SAT 2006 conference. See the PB'06 web page for
the deadlines and new rules.
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 firstname.lastname@example.org.
Results of the evaluation
The evaluation was performed in two steps. The first phase which took
place from April to June 2005 allowed to run several versions of the
solvers and to detect the first bugs in the solvers
implementation. Unfortunately, the bug correctives that were submitted
by the authors still had some bugs. Therefore, the results that were
presented to the SAT conference in June 2005 were not completely
satisfying since every solver had at least a problem (but some of
these problems where simple mistakes in the solvers output).
To obtain more reliable results, it was decided to run the solvers
one last time in September. Authors were allowed to fix the bugs as
well as to improve their solver. During this second phase, only one
version of the solvers was allowed to run.
Keep in mind that this event was an evaluation instead of a
competition. Our goal was to take a snapshot of the current state of
art rather than to obtain a ranking of the different solvers (because
we couldn't get it right on our first try).
Eight solvers (with several variants or versions) were submitted to
|| Vasco Manquinho and João Marques-Silva
|| Donald Chai and Andreas Kuehlmann
|| Niklas Eén and Niklas Sörensson
|| Fadi Aloul and Bashar Al-Rawi
|| Olivier Bailleux, Yacine Boufkhad, Olivier Roussel
|| Hossein Sheini and Karem Sakallah
|| Daniel Le Berre, Mederic Baron, Anne Parrain, Olivier Roussel
|| Daniel Vallstrom
- Benchmarks used during the evaluation are available here.
- The call for solvers and benchmarks is archived here.
The authors are greatly indebted to Daniel Le Berre and Laurent Simon
for providing the scripts of the SAT competition, to the LINC Lab,
Department of ECECS, University of Cincinnati for providing the
computing resources and to Robert Montjoy for his assistance. Special
thanks to Michal Kouril for his great help and his continuous interest
in this evaluation.
The second pseudo-Boolean evaluation is organized as a special event of
the SAT 2006 conference.
See the PB'06 web page
for the deadlines and new rules.
To reach the organizers, send an email to email@example.com.
INESC-ID, Lisboa, Portugal
vmm at sat.inesc.pt / home page
CRIL, Université d'Artois, France
cril.univ-artois.fr / home page