Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013

Abstract

Abstract—This paper serves as solver description for our SAT solver Lingeling and its two parallel variants Treengeling and Plingeling entering the SAT Competition 2013. We only list important differences to the version of these solvers used in the SAT Challenge 2012. For further information we refer to the solver description [1] of the SAT Challenge 2012 or source code. LINGELING The differences on the search side, that is during the CDCL loop, are as follows. The inner-outer scheme for reduce scheduling is not enabled by default, but only enabled dynamically, if the number of remaining variables drops below 1000. It also turned out that the previous VMTF decision scheduler, though faster to compute, is less robust, and occasionally leads to time-outs on otherwise easy to satisfy instances. Thus we went back to the exponential VSIDS scheme of MiniSAT.