2003 Winners now known!!!
The online
report will be updated with all the details of the second
stage, plus an analysis of the competition. For now, one can take a
look at our slides (PPT,
PDF)
from the SAT2003
conference and the
detailled results of the first stage.
Industrial category
We have a local copy of the industrial benchmarks: sc2003benchs.zip.
Forklift, from from Eugene Goldberg and Yakov Novikov (complete
deterministic) won both the "best complete solver on industrial benchmarks"
and "best solver on satisfiable industrial benchmarks" awards.
Forklift is a new solver that can be viewed as an
extension of Berkmin62 with limited resolution at each leaf.
Handmade category
satzoo from Niklas
Een (complete deterministic) won both the "best complete solver on
handmade benchmarks" and "best solver on satisfiable handmade
benchmarks" awards.
Satzoo is a Chaff-like SAT-solver based on watched
literals and clause recording. It was
developed mainly to be able to experiment with new model checking
techniques which requires a tighter integration with the SAT-solver.
As such, Satzoo takes a more general view on what a ``SAT" problem
could be, and supports solving a number of related SAT-problems by
an incremental SAT interface. Satzoo is also
meant to encompass more types of constraints than just clauses. To
prototype this, linear constraints over boolean
variables were added to the solver. The front end thus
supports a subset of the CPLEX lp-format along with DIMACS
cnf-format. For lp-files optimization is performed towards the goal
function rather than just finding a satisfying assignment.
Random category
kcnf
from Gilles Dequen and Olivier Dubois won the "best complete solver on
random benchmarks" award.
unitwalk from
Edward Hirsch and Arist Kojevnikov (Incomplete randomized) won the "best solver
on satisfiable random benchmarks" award.
UnitWalk is a combination of unit clause elimination (particularly,
the idea of Paturi, Pudlak and Zane's randomized unit clause
elimination algorithm) and local search. The solver
participated in the competition extends this basic algorithm with
adding some of 2-resolvents using incBinSat, and mixes
its random walks with WalkSAT-like walks.
benchmarks awards
The benchmarks from the SAT2002 competition not solved during the
first stage were used in this year competition as "SAT2002
competition challenging benchmarks". Those benchmarks were submitted
last year, so they cannot be awarded this year.
Smallest unsatisfiable benchmark:
random/hirsch/hgen8/hgen8-n260-01-S1597732451
(260 variables, 391 clauses, 888 literals)
Smallest satisfiable benchmark:
random/simon/sat02-random/hgen2-v400-s161064952 (400 variables, 1400
clauses, 4200 literals). There is no award for that benchmark since
it is one of the SAT2002 competition challenging benchmarks. Note
that last year, unitwalk solved it during the second stage in 20199s
on a PIII 450 (this year the timeout was 7200s on an Athlon 1800+).
Last update: 19 may 2003