[  news | medals | download | older-versions | license | papers | background ]

News

The latest version can be found on GitHub: https://github.com/arminbiere/lingeling.

The parallel portfolio front-end Plingeling was ranked on the first place on unsatisfiable instances in the parallel track of the SAT Competition 2020, and second place overall in the parallel track.

Version bcj was the first to be released under MIT style license.

Medals

SAT'16 Competition version of Lingeling, Plingeling and Treengeling in one archive: lingeling-bbc-9230380-160707.tar.gz and with proof support lingeling-bbc-9230380-160707-druplig-009.tar.gz.

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 and its parallel versions Plingeling and Treengeling, obtained first places in 4 tracks (out of 11) of the SAT'14 Competition and thus won 4 Gödel medals during the FLoC'14 Olympic Games.

A summary of the competition can be found in the slides of the presentation of Marijn Heule announcing the results at the SAT'14 conference.

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.

Download

[ lingeling-bcj-78ebb86-180517.tar.gz ] SAT Competition 2018 version (essentially)
[ lingeling-bbc-9230380-160707.tar.gz ] SAT Competition 2016 version
[ lingeling-bal-2293bef-151109.tar.gz ] SAT'15 Race Version (without ML)
[ lingeling-baq-e70d097-151109.tar.gz ] SAT'15 Race (with ML)
[ lingeling-b85-3ee2a39-151109.tar.gz ] Boolector SMT'15 Version

Older Versions

We provide the original archives for the different variants of Lingeling as submitted to the SAT'14 Competition and CSSC'14 in the format as required by the competition organizers:

[ lingeling-ayv-86bf266-140429.zip ]
[ lingeling-druplig-azd-0d99752-140506.zip ]
[ plingeling-ayv-86bf266-140429.zip ]
[ treengeling-ayv-86bf266-140429.zip ]
[ lingeling-cssc14.tar.gz ]

Intermediate release ats1

[ lingeling-ats1-ce8c04f-140207.tar.gz ]

SAT Competition 2013 versions which won 7 medals in the SAT'13 competition:

[ lingeling-aqw-27d9fd4-130429.zip ]
[ plingeling-aqw-27d9fd4-130429.zip ]
[ treengeling-aqw-27d9fd4-130429.zip ]

Even older versions:

[ lingeling-ala-b02aa1a-121013.tar.gz ]
[ lingeling-al6-080d45d-120922.tar.gz ]
[ lingeling-587f-4882048-110513.tar.gz ]
[ lingeling-276-6264d55-100731.tar.gz ]

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.

The README and COPYING files for version bcj are available separately.

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.

License

Newer version, starting with the SAT Competition 2013 version aqw use a restricted license for non-commercial use.

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.

Papers

Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions, Tomas Tomáš, Marijn Heule, Matti Järvisalo (editors), vol. B-2017-1 of Department of Computer Science Series of Publications B, pages 14-15, University of Helsinki, 2017.
[ paper | bibtex ]

Armin Biere. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Matti Järvisalo (editors), vol. B-2016-1 of Department of Computer Science Series of Publications B, pages 44-45, University of Helsinki, 2016.
[ paper | bibtex ]

Tomas Balyo, Armin Biere, Markus Iser, Carsten Sinz. SAT Race 2015, in Journal of Artificial Intelligence, vol. 241, pages 45-65, Elsevier 2016.
[ preprint | bibtex | web | ipasir.zip | ipasir.h ]

Armin Biere. Yet another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014. In Proceedings of SAT Competition 2014, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2014-2 of Department of Computer Science Series of Publications B, pages 39-40, University of Helsinki, 2014.

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.

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, 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.

Background

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.cs.ubc.ca/~hoos/SATLIB. 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.