The competitors

Solver submission closed on February 14th. Late submissions were accepted if the solvers complied with input/output requirements. Those solvers entered the first stage, which allowed them to compete with current state-of-the-art SAT solvers, without being awardable. Those solvers are tagged ``hors concours''.

amvo

from Sean Vogt and Andrew Machen (incomplete, randomized).

berkmin

(release 561 and release 62) from Eugene Goldberg and Yakov Novikov [11] (complete, deterministic). 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. Bermin561 binaries are available at http://eigold.tripod.com/BerkMin.html. Berkmin62 was awarded ``best solver on satisfiable handmade benchmarks'' at SAT2002 competition.

bmsat

(BlueMoonSAT, hors concours) from Xiaowei Xu (complete, deterministic). The solver is hors concours because that version of bmsat was submitted after the deadline, on March 7.

compsat

(release 0.5) from Armin Biere (complete, deterministic). zchaff like solver with very compact memory footprint that uses van Gelder's approach for watching literals[26] and dynamically compressed stacks for saving memory. Builtin proof checker in debugging mode. Solid test frame work.

farseer

(release 1.00), from Martin Girard (complete, deterministic). Hybrid core with implicative closure, dependency-directed backtracking and enhanced local search. The latter is used as 'intuition' for branching. It is an experiment to determine how an algorithm with a lot of overhead would perform in the long run for practical unsolved problems.

forklift

from Eugene Goldberg and Yakov Novikov (complete deterministic). Forklift is a new solver that can be viewed as an extension of Berkmin62 with limited resolution at each leaf.

funex

(release 0.2) from Armin Biere.

• integers for literals
• separate clause data structure
• constant time lookup of the 'other' watched literal
• early conflict detection
• simplifications of reasons
• Horn, DLIS, Berkmin, Chaff strategy
• cache for satisfied clauses
• decision strategy as omega regular expression
• builtin proof checker in debugging mode
• solid test frame work

jerusat

(release 1.1 va, vb, vc) from Nadel Alexander [2] (complete, deterministic). Jerusat 1.1 implements the CRSAT algorithm which is an extension of DPLL and also CRSAT-related pruning techniques. It also uses VAP heuristics; WLCC data structure; ``literals' density" relevance-based learning and currently undocumented restart strategy. Binaries available at http://www.geocities.com/alikn78/

jquest2

from Inês Lynce - João Marques Silva [4] (complete, deterministic). This solver is implemented in Java and incorporates the following features:

• Watched literals-like data structures [4].
• VSIDS-like branching heuristic [20].
• GRASP-like clause recording and non-chronological backtracking[19]. Clause recording stops at the first UIP [20].
• Search restart strategy [12] based on an initial threshold that is repeatedly incremented to guarantee completeness [5]

JQuest2 is an OpenSAT-compliant solver [3].

kcnfs

from Gilles Dequen and Olivier Dubois [10,9] (complete, deterministic). kcnfs source code is available at http://www.laria.u-picardie.fr/~dequen/sat/.

limmat

(release 1.3) from Armin Biere (complete, deterministic).

• zchaff like solver
• constant time lookup of the 'other' watched literal
• early conflict detection
• simplifications of reasons
• builtin proof checker in debugging mode
• solid test frame work

Source code available at http://www.inf.ethz.ch/personal/biere/projects/limmat. Limmat was awarded ``Best solver on satisfiable industrial benchmarks'' at SAT2002 competition.

lsat

(release 1.1) from Richard Ostrowski, Bertrand Mazure and Lakhdar Sais (complete, deterministic) [21]. LSAT detects some boolean functions (equivalency chains, and/or gates) and uses them

1. to simplify the original CNF
2. to detect independent variables.

Then a classical DPLL is launched on the simplified CNF, branching only on independent variables. lsat (v 1.0) participated to the SAT2002 competition.

march sp/tt/xq

from Mark Dufour, Marijn Heule, Joris van Zwieten and Hans van Maaren (complete, deterministic). Preprocessing with equivalence reasoning, a 3-sat translator and adding resolvents. Partial lookahead. Selection of variables for lookahead is based on a prediction of the amount of new 2-clauses they will generate. Tree based lookahead using a timestamp oriented data structure. Local learning.

oepir

Oepir (release 0.2) from Johan Alfredsson (complete, deterministic). Oepir is basically a standard DLL solver in the spirit of Chaff[20] and BerkMin[11]. In does not feature many bells and whistles yet, but includes a semi-automatic strategy selection mechanism and has the ability to solve incremental problems.

oksolver

(hors concours) from Oliver Kullmann (complete, deterministic) [14]. Source code available at http://cs-svr1.swan.ac.uk/~csoliver/ Oksolver was awarded both ``best complete sat solver on random benchmarks'' and ``best solver on satisfiable random benchmarks'' at SAT2002 competition. oksolver was not submitted to the competition but it is entering the competition on random category as the winner of the previous competition.

opensat

(release 0.44) from Gilles Audemard, Daniel Le Berre and Olivier Roussel [3] (complete deterministic). This solver, in Java, uses the reference implementation of several techniques from the OpenSAT project:

• Watched Literals data structure[20].
• Relsat[7] non chronological backtracking (backjumping).
• VSIDS-like heuristic[29] on conflicting clauses.
• learning of small clauses only (4 literals or less): unlike GRASP[18], Chaff[20], Berkmin[11], etc., learning is not necessary for backtracking.
• Rapid Restart Strategy[12] based on conflicts: restart threshold starts at 100 conflicts and increases by 1.5 at each restart.

More information about the OpenSAT project is available at http://www.opensat.org/.

qinting

(release 1.0) from Xiao Yu Li, Matthias F. Stallmann and Franc Brglez [17] (incomplete randomized). QingTing uses the UnitWalk algorithm with Zhang Hantao's unit propagation algorithm and Zchaff's watched literal lazy data structure. QingTing source code is available at http://pluto.cbl.ncsu.edu/EDS/QingTing/.

satnik

from Niklas Sörensson (complete deterministic).

sato

(release 3.4) from Hantao Zhang (complete deterministic) [28].Sato is a propositional solver based on the Davis-Putnam-Logemann-Loveland method [8]. Sato uses the head-tail data structure (with reset) for efficient unit propagation and lemma learning for dependency-directed backtracking. The new feature of this release is its capacity of handling a special predicate of clauses: Constraints over the number of true literals in a clause. This feature allows sato to solve efficiently max-sat, max-one, and other problems.

saturn

(release 2) from Steven Prestwich. (Incomplete, randomized). [23]. Saturn performs local search in a space of partial truth assignments that are consistent under unit propagation. It is a DPLL procedure with depth-first search replaced by an incomplete form of backtracking (Incomplete Dynamic Backtracking). Saturn release 1 participated to the SAT2002 competition. The difference between version 2 and version 1 is a form of conflict diagnosis: variables are selected for unassignment by analysing the causes of dead-ends during search (to be described in future work).

satzilla

(release 0.9, v1 v2) (v2 is hors concours) from Kevin Leyton-Brown,Eugene Nudelman, Galen Andrew, Carla Gomes, Jim McFadden, Bart Selman and Yoav Shoham (complete, randomized).

Our solver takes an unusual, "portfolio" approach to the SAT problem. Instead of implementing a novel SAT algorithm from scratch, Satzilla uses machine learning models to select among a set of existing SAT algorithms, and then runs the algorithm predicted to do best. This approach is motivated by the observation that different algorithms often perform well on different problem inputs. This means it is possible for a portfolio that selects from a set of algorithms to outperform each of its constituent algorithms. Here is how Satzilla uses our portfolio approach to solve SAT instances: First, it computes about 60 polynomial time features of the instance that are indicative of runtime. These include:

• simple features like the number of variables and clauses, and clause to variable ratio
• statistics (mean, stddev, min, max, entropy) of the number of clauses in which each variable participates
• statistics and clustering features of the clause-graph (a graph whose nodes are clauses with an edges between clauses in which one clause contains a literal and the other clause contains its negation)
• statistics from an LP relaxation of the SAT problem
• probing features that sample data from iterations of local search and DPLL

It then uses linear regression models of these features to predict the run time for each of its constituent algorithms. For Satzilla 0.9, these include: 2clseq, Limmat, JeruSat, OKsolver, Relsat, Sato, Satzrand, and Zchaff. It then runs the algorithms with the lowest predicted run time.

Our Hors Concours solver satzilla2 (submitted after the deadline, on February 28) uses two additional complete solvers, Eqsatz and Heerhugo. It also executes the AutoSat algorithm for a short time before starting any other computation, and is thus able to filter out easy satisfiable problems.

Unfortunately, the predictive models that were submitted with the two solvers were trained on a renormalized set of features. This addition of noise means that the algorithm selection performed by both Satzillas is not nearly the same as it would be with correct runtime models.

The techniques for predicting run time of algorithms are described in [16]. The portfolio approach (with experimental results examining a different problem domain) is elaborated in [15].

satzoo

(release 0.98 v0 v1) from Niklas Een (complete deterministic). Satzoo is a Chaff-like SAT-solver based on watched literals[20] and clause recording[19]. 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[27]. Satzoo is also meant to encompass more types of constraints than just clauses. To prototype this, linear constraints over boolean variables[6] 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. More infos available at http://www.cs.chalmers.se/~een/Satzoo/

siege

(hors concours) from Lawrence Ryan (complete, randomized). Siege is a highly robust solver featuring (a) fast BCP through degenerate watched literals; (b) improved locality through clause compression; (c) frequent heuristic backtracking; and (d) a new and extremely simple O(1) decision strategy that typically accounts for less than 0.5% of the runtime. Binaries are available at http://www.cs.sfu.ca/~loryan/personal/. That solver is hors concours because it was submitted after the deadline.

tts

(ternary tree solver, release 1.0, hors concours) from Ivor Spence (complete, deterministic). A ternary tree is constructed which represents the search space. This tree is traversed to search for a satisfying assignment. Each time an assignment yields false the reasons for this correspond to a set of nodes in the tree which is recorded. Further walks which encounter this same set can be pruned immediately. That solver is hors concours because it was submitted after the deadline, on March 7.

unitwalk

(release 0.981) from Edward Hirsch and Arist Kojevnikov [13] (Incomplete randomized) UnitWalk is a combination of unit clause elimination (particularly, the idea of Paturi, Pudlák and Zane's randomized unit clause elimination algorithm [22]) and local search. The solver participated in the competition extends this basic algorithm with adding some of $2$-resolvents using incBinSat [30], and mixes its random walks with WalkSAT-like [24] walks. The version 0.98 participated to the SAT2002 competition. Available in source (C) at http://logic.pdmi.ras.ru/~arist/UnitWalk/.

xqinting

(release 0.1) from Xiao Yu Li, Matthias F. Stallmann and Franc Brglez (complete randomized). xQingTing is a complete solver based on DPLL. It uses Zchaff-like decision heuristic and watched literal lazy data structure. It doesn't use learning (clause recording); therefore, it only does chronological backtracking.

zchaff from Yinlei Yu and Lintao Zhang [20,29] (complete deterministic). zchaff is a carefully engineered DPLL with non-chronologicial backtracking, learning (clause recording), restarts, randomized branching heuristic and an innovative notion of ``heuristic learning'' (VSIDS). zchaff source code is available at http://www.cs.princeton.edu/~chaff. zchaff was awarded best complete solver for both industrial and handmade categories at SAT2002 competition.