Solver Submission

We wanted the competition to be as fair and open as possible. So we did not want to restrict people to a given language (such as C or C++): the only condition was that the solver can run on a standard Linux/Unix box. The solver sources had to be provided, with a suitable makefile. Additional libraries were statically linked to the code. All but one solvers were in C/C++, one was in Java.

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 $2$-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.

Then a classical DPLL is launched on the simplified CNF, branching only on 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.