Lingeling and Friends at the SAT Competition 2011
Armin Biere
Abstract
Abstract. This note serves as system description for our solvers submitted to the various tracks of the SAT Competition 2011 affiliated to the SAT conference 2011. Overview To the main track of the SAT Competition 2011 we submitted the new version 587 of our SAT solver Lingeling and its parallel extension Plingeling [1]. To the minimally unsatisfiable subset track we submitted front-ends of PicoSAT version 941, one for each of the sub-tracks. The plain MUS front-end PicoMUS uses multiple rounds of randomized clausal core extraction as preprocessing step before switching to selector variable based core minimization. The group-oriented MUS extractor PicoGCNF only uses the latter technique, which is actually available as new API function in the PicoSAT library and computes a minimal subset of failed assumptions for assumption based incrememental SAT solving. In order to use the clausal core feature, PicoSAT is compiled with proof tracing support, which is expected to slow down plain solver speed. Thus, for comparison, we submitted this version of PicoSAT also to the main track of the competition. To the MiniSAT hack track we submitted a version of MiniSAT 2.2.0 which uses our agility metric [3] to control when to disable backtracking during restarts with agility limit 26%. 1 Lingeling 587 The version of Lingeling submitted to the competition differs from the version submitted to the SAT Race 2010 described in [1] as follows. Similar to CryptoMiniSAT [7] our new garbage collection algorithm for reducing the number of learned clauses determines at run-time whether classic activity based heuristics or glues [2] are used. When a reduction operation is scheduled the average and standard deviation of the glue values of the still existing learned redundant clauses are computed. From this information the solvers tries to determine