LINGELING and Friends Entering the SAT Challenge 2012
Armin Biere · 2012
I. LINGELING Compared to the version submitted to the SAT competition 2011 and described in [1], we removed complicated algorithms and features, which did not really have any observable impact on the run-time for those benchmarks we tried. In particular, various versions of distillation inprocessors were removed. Regarding inprocessing [4], there are two new probing variants. One is called simple probing and tries to learn hyper binary resolutions eagerly. The other variant is based on tree-based look-ahead, which is a simplified version of the implementation in March [2]. These two techniques are complemented by gaussian elimination and a new congruence closure algorithm, which both use extracted gates to generate and propagate equivalences. We also switched to one merged inprocessing phase, called