Lingeling, Plingeling and Treengeling
In the recent SAT'15 Race the parallel front-ends Plingeling and Treengeling of Lingeling obtained 2nd and 3rd place in the parallel track. The base sequential version of Lingeling won the prize most innovative solver.
Lingeling also won a first place in the Configurable SAT Solver Challenge (CSSC'14)
Beside these four first places, variants of Lingeling were placed 2nd four times and 3rd placed once in the SAT'14 Competition, thus altogether 9 times among the first three.
The latest publically available versions as used in the recent SAT'15 Race. For usage outside of a SAT competition/race setting you might want to use the plain version bal which does not try to classify benchmarks according to the SAT'14 Competition buckets using machine learning.
Intermediate release ats1
Even older versions:
Version al6 is a stripped down and slightly improved variant of version agm submitted to the SAT Challenge 2012, which is currently not available publically. The main differences compared to agm are on the positive side an improved reduce scheduler (similar to 587f), and on the negative side the removal of two yet unpublished probing techniques.
Version 587f won 4 medals in the SAT Competition 2011 including a gold medal in the parallel application track on multi-core machines for Plingeling. It was running hors concours in the SAT Challenge 2012 and would have won the application single engine track.
Version 276 was the first cleaned up public release. It is almost identical to version 271 of Lingeling and Plingeling, which was used in the SAT Race 2010. Lingeling was ranked second in the main track and Plingeling ranked first in the parallel track.
By default it is also prohibited to use these newer version of Lingeling as part of a competition, without explicit written permission.
Old versions of the source code of Lingeling and Plingeling were and still are available under GPL.
For other licenses contact Armin Biere.
The C API of Lingeling has its origin in the one of PicoSAT. The header file of PicoSAT is much better documented than the one of Lingeling. Thus you might want to consult the header files of both solvers. There is also a slide set from a tutorial on using PicoSAT which contains actual C code.
A. Biere. Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In Proceedings of SAT Competition 2013, A. Balint, A. Belov, M. Heule, M. Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 51-52, University of Helsinki, 2013.
A. Biere. Lingeling and Friends Entering the SAT Challenge 2012. In Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions, A. Balint, A. Belov, A. Diepold, S. Gerber, M. Järvisalo, and C. Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 33-34, University of Helsinki, 2012.
A. Biere. Lingeling and Friends at the SAT Competition 2011. Technical Report 11/1, March 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
A. Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, August 2010, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
SAT is the classical NP complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF). The Handbook of Satisfiability gives an excellent overview of theoretical and practical aspects of the field.
Further information on SAT can be found at www.satlive.org or www.satlib.org. We also have some papers on SAT mostly focusing on practical SAT solving. On our software page you find earlier SAT solvers and related tools by our group.