SAT2002 competition news


Last modifications: September 11, 2002

Check out the competition report here: HTML, PS, PDF.

More news concerning March solvers:
The heuristics used in the March solvers can be found in the paper: Solving satisfiability problems using elliptic approximations: effective branching rules by Joost Warners and Hans van Maaren (Discrete Applied Mathematics 107 (2000), 241-259)

Award summary

More detailed infos coming soon!!!!!

Best performance of a complete solver on industrial benchmarks

ZCHAFF, from Lintao Zhang and Sharad Malik
Description:
M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver, 38th Design Automation Conference (DAC'01), June 2001, pp. 530-535.
L. Zhang, C.F. Madigan, M.W. Moskewicz, and S. Malik, Efficient Conflict Driven Learning in a Boolean Satisfiability Solver, International Conference on Computer-Aided Design (ICCAD '01), November 2001, pp. 279-285.

Best performance of a solver on satisfiable industrial benchmarks

LIMMAT, from Armin Biere
Description:
No paper available. Quoted from the author:
zchaff-like SAT solver with:
  1. early detection of conflicts in the BCP queue
  2. constant time lookup of the 'other' watched literal
  3. optimized ordering of decision variables
  4. implemented in C 5. robust code through sophisticated test framework
Get Limmat source code here

Best performance of a complete solver on handmade benchmarks

ZCHAFF, from Lintao Zhang and Sharad Malik
Description: as above

Best performance of a solver on satisfiable handmade benchmarks

BERKMIN, from Eugene Goldberg and Yakov Novikov
Description:
E. Goldberg, and Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Design, Automation, and Test in Europe (DATE '02), March 2002, pp. 142-149.

Best performance of a complete solver on random benchmarks

OKSOLVER, from Oliver Kullmann
Description:
Heuristics for SAT algorithms: Searching for some foundations. September 1998, 23 pages. (Updated September 1999 w.r.t. running times.)

Best performance of a solver on satisfiable random benchmarks

OKSOLVER, from Oliver Kullmann
Description: as above.

Smallest unsolved unsatisfiable instance:

xor-chains, from Lintao Zhang and Sharad Malik
Description: 106 variables, 282 clauses, 844 literals, Verification problem of 2 xor chains

Smallest unsolved satisfiable instance:

generated from hgen-2, from Edward A. Hirsch
Description: 500 variables, 1750 clauses, 5250 literals randomly generated 3-CNF, clause/variables ratio=3.5
  1. balanced number of literal occurrences (no literal occurs much more frequently than others)
  2. literals forcing the satisfying assignment are less frequent
  3. Formula does not contain clauses C_1, C_2, C_3 such that C_1 contains variables a,b; C_2 contains variables b,c; C_3 contains variables a,c.

First stage results

We are now ready to unveil the first stage results.

Some solvers reported UNSAT on SAT instances: we decided to put them hors-concours, which means that they won't go to the next stage, and that we will not consider their results for the awards.
Here is the list of those solvers:


Note that most of the time these solvers worked fine and that their unexpected behavior is localized to a few families of benchmarks only.

One solver gave wrong SAT certificates for some instances. We decided to consider these instances as unsolved.

List of submitted benchmarks

Here is the list of submitted benchmarks.

Benchmarks submission

We have 901 generated benchmarks (with automatically submitted satex challenging instances and 2 sub-families from Miroslav Velev's BMC) in 41 groups.

11 different random-generators (all looking "more or less" like 'k-SAT uniform' generators, some force the instance to be satisfiable).

We have two others non-random generators in addition.

Solvers submission

19 author groups submitted 30 solvers: 28 were accepted for the competition in which 3 are 'hors-concours'*, 2 solvers were rejected after the test phase.

Among the 28 solvers:

The solvers are written in C/C++, except one in JAVA.

* The 3 solvers running 'hors-concours' have been modified after the bug-testing stage by their authors while were not found buggy by the competition organizing committee.

List of competing solvers (no particular order) 
Armin BIERE limmat (compl. det.)

Steven PRESTWICH saturn (incompl. rand.)

Fahiem BACCHUS 2clseq  (compl. det.) 

Marijn HEULE (Hans vanMAAREN, Mark DUFOUR, Joris vanZWIETEN) marchI,marchIse,marchII,marchIIse  (compl. det.)

Anatoly PLOTNIKOV (Stas BUSYGIN) blindsat (compl.  det.)

Anton EREMEEV (Pavel BORISOVSKY) ga (incomp.  rand.)

Eugene GOLDBERG (Yakov NOVIKOV) berkmin (comp. det.)

Edward HIRSCH (Arist KOJEVNIKOV) unitwalk (incomp.  rand.)

Joao MARQUES-SILVA (Inês LYNCE) jquest (comp. rand)

Richard OSTROWSKI (Bertrand MAZURE, Lakhdar SAIS) lsat (comp. det.)

Bu DONGBO usat05,usat10 (incomp. rand.)

Hantao ZHANG sato (comp. rand.)

Armando TACCHELLA (Enrico GIUNCHIGLIA, Massimo MARATEA) simo (comp. rand.) 

Oliver KULLMANN oksolver (comp. det.)

Benjamin WAH (Alan ZHE WU) dlmsat1,dlmsat2,dlmsat3 (incomp. rand.)

Allen VANGELDER rb2cl,modoc (comp. det.)

Lintao ZHANG (Sharad MALIK) chaff (comp. det.)

John KOLEN partsat (comp. det.)


Hors-concours:
Marijn HEULE (Hans vanMAAREN, Mark DUFOUR, Joris vanZWIETEN),marchIse-hc,marchII-hc,marchIIse-hc (compl.  det.)

The competition

The competition started April 8, 2002 on a cluster of 30 Bi-Pentium III (and not II as previously stated) 450 Mhz with 1Gb of RAM under Linux. Only one processor is used for running the competition.

Each solver is given 40 minutes and 900Mb to solve an instance.

As soon as we have first results to be published, we'll made them available on the web (using satex publishing framework).

http://www.lri.fr/~simon/satex/competition

                The organizing committee

[ SAT2002 Competition] [ SAT 2002] [SAT-Ex ] [SATLIB] [ SAT Live!]