**limmat**- Armin Biere. Complete deterministic solver. This is a
zchaff-like SAT solver (implemented in C) with an early detection of
conflicts in the BCP queue; a constant time lookup of the 'other'
watched literal; an optimized ordering of decision variables and a
robust code through sophisticated test framework. More informations
and sources are available at
`http://www.inf.ethz.ch/personal/biere/projects/limmat/`. **saturn**- by Steven Prestwich [Pre02b].
Incomplete randomized solver.
**2clseq**- by Fahiem Bacchus. Complete deterministic solver. DPLL with
binary clause and equivalence reasoning plus intelligent backtracking
and learning
[Bac02a,Bac02b]. Available in source (C++) at
`http://www.cs.toronto.edu/~fbacchus/2clseq.html`. **marchI, marchIse, marchII, marchIIse**- by Marijn Heule, Hans van
Maaren, Mark Dufour, Joris van Zwieten. Complete deterministic
solver. Those solvers were designed by postgraduate students for a
course given by Hans van Maaren. The heuristics used in those solvers
can be found in [WvM00]. Note that some of them
(marchIse-hc, marchII-hc, marchIIse-hc) were received after the
deadline so we decided to run them hors-concours.
**blindsat**- by Anatoly Plotnikov and Stas Busygin. Complete
deterministic solver. A report and the solver source (C++) are
available at
`http://www.vinnica.ua/~aplot/current.html`. **ga**- by Anton Eremeev and Pavel Borisovsky. Incomplete randomized
solver. A greedy crossover genetic algorithm.
**berkmin**- by Eugene Goldberg and Yakov Novikov [GN02]. Complete
deterministic solver.
*Berkmin inherits such features of GRASP, SATO, and Chaff as clause recording, fast BCP, restarts, and conflict clause ``aging''. At the same time Berkmin introduces a new decision making procedure and a new procedure for the management of the database of conflict clauses. The key novelty of Berkmin is that this database is organized as a chronologically sorted stack. Berkmin always tries to satisfy the topmost unsatisfied clause of the stack. When removing clauses Berkmin tries to get rid of the clauses that are at the bottom of the stack in the first place.*[Eugene Goldberg] The version used for the competition was 62. Berkmin 56 binaries are available at`http://eigold.tripod.com/`. **unitwalk**- by Edward A. Hirsch and Arist Kojevnikov [HK01].
Incomplete randomized solver.
UnitWalk is a combination of unit clause
elimination (particularly, the idea of Paturi, Pudlák and Zane's
randomized unit clause elimination algorithm [PPZ97]) and local
search. The solver participated in the competition extends this
basic algorithm with adding some of -resolvents using incBinSat
[ZS02], and mixes its random walks with WalkSAT-like
[SKC94b] walks. The version used for the competition was
0.98. Available in source (C) at
`http://logic.pdmi.ras.ru/~arist/UnitWalk/`. **jquest**- by Joao Marques-Silva and Inês Lynce. Complete
deterministic solver. Jquest is a SAT platform in Java containing
various heuristics, data structures and search strategies
[LaPMS02]. The solver was configured with lazy data
structures (inspired by both SATO and Chaff), non-chronological
backtracking and clause recording (like in Grasp), chaff-like
heuristic, randomized backtracking [LBaPMS01] and rapid
restarts strategy. JQuest source code is available at
`http://sat.inesc.pt/sat/soft/jquest/jquest-src.tgz` **lsat**- by Richard Ostrowski, Bertrand Mazure and Lakhdar Sais
[OGMS02]. Complete deterministic. LSAT
detects some boolean functions (equivalence chains, and/or gates) and
uses them
- to simplify the original CNF,
- to detect independent variables.

**usat05, usat10**- by Bu Dongbo. Incomplete randomized solver. No
description available.
**sato**- by Hantao Zhang [Zha97]. Complete deterministic solver.
**simo**- by Armando Tacchella, Enrico Giunchiglia, Marco Maratea [CFG$^+$01].
Complete deterministic (wrongly noted randomized in the
competition). In Simo3.0 there are features the most recent and effective
in SAT like UIP-based learning, restart, 2-literals watching. Simo3.0 is
characterized by a new type of heuristic(called GMT). GMT tries to
combine Chaff-like and SATZ-like heuristics. The idea is to switch between
SATZ-like and Chaff-like heuristics by introducing measures of
``probably successful search" and ``probably unsuccessful search".
The default is to use a Chaff-like heuristic. When the measure
of unsuccessful search exceeds a given threshold, SIMO switches
to a SATZ-like heuristic. SIMO resumes the Chaff-like heuristic once
the measure of successful search exceeds a given threshold.
SIMO 2.0 is available in source (C++)
at
`http://www.mrg.dist.unige.it/~sim/simo/`. **OKsolver**- by Oliver Kullmann [Kul02b]. Complete deterministic solver.
*OKsolver has been designed to be a "clean solver" as possible, minimising the use of "magical numbers", and for 3-CNF indeed the algorithm is completely generic. OKsolver is a DPLL-like algorithm, with reduction by failed literals (complete and iterated at each node) and autarkies (found when searching for failed literals), while the branching heuristic chooses a variable creating as many new clauses as possible (exploiting full unit clause propagation for all variables), and the first branch is chosen maximising an approximation of the probability, that a branching formula is satisfiable*[Oliver Kullmann]. OKsolver 1.2 source code is available at`http://cs-svr1.swan.ac.uk/~csoliver/` **dlmsat1, dlmsat2, dlmsat3**- by Benjamin Wah and Alan Zhe
Wu [SW98]. Incomplete randomized solvers. Available in
source at
`http://manip.crhc.uiuc.edu/Wah/programs/SAT_DLM_2000.tar.gz`. **modoc**- by Allen Van Gelder
[VG99,VGO99,OVG00].
Complete deterministic solver.
Binaries available
at
`ftp://ftp.cse.ucsc.edu/pub/avg/Modoc/`. **rb2cl**- by Allen Van Gelder.
[VT96,VG02a,VG02b].
Complete deterministic solver.
*It applies reasoning in the form of certain resolution operations, and identification of equivalent literals. Resolution produces growth in the size of the formula, but within a global quadratic bound; most previous methods avoid operations that produce any growth, and generally do not identify equivalent literals. Computational experience so far suggests that the method does substantially less "guessing" than previously reported algorithms, while keeping a polynomial time bound on the work done between guesses.*[Allen van Gelder] **zchaff**- by Lintao Zhang and Sharad Malik [MMZ$^+$01,ZMMM01].
Complete deterministic solver. This solver is a carefully engineered DPLL
procedure with non-chronological backtracking, learning (clause recording),
restarts, randomized branching heuristic and an innovative notion of
``heuristic learning'' (VSIDS). Zchaff source code is available at
`http://www.ee.princeton.edu/~chaff` **partsat**- by John Kolen. Complete deterministic solver. No description available.