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