Lingeling, Plingeling and Treengeling

News

New version ats1.

SAT Competition 2013 version aqw.

For more information on the competition version see the system description.

Download

Latest version ats1

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

Version ats1 fixes a bug in the new backward subsumption code when importing units through 'syncunits' call backs, introduced in the previous release ats. This affects Plingeling and might affect Treengeling too (unconfirmed).

SAT Competition 2013 versions which won 7 medals:

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

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 NEWS files for version ats 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

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.

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