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)

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.

Description:

No paper available. Quoted from the author:

- early detection of conflicts in the BCP queue
- constant time lookup of the 'other' watched literal
- optimized ordering of decision variables
- implemented in C 5. robust code through sophisticated test framework

Description: as above

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.

Description:

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

Description: as above.

Description: 106 variables, 282 clauses, 844 literals, Verification problem of 2 xor chains

Description: 500 variables, 1750 clauses, 5250 literals randomly generated 3-CNF, clause/variables ratio=3.5

- balanced number of literal occurrences (no literal occurs much more frequently than others)
- literals forcing the satisfying assignment are less frequent
- 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.

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:

- lsat
- MarchI, MarchIse
- partsat
- sato

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.

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.

Among the 28 solvers:

- 17 complete deterministic solvers
- 11 randomized solvers

in which 8 solvers are incomplete.

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

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.)

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!]