Lingeling and Plingeling

News

SAT Competition 2011 version 587f released.

Version 276 was the first public release.

Download

[ lingeling-587f-4882048-110513.tar.gz | lingeling-276-6264d55-100731.tar.gz ]

Version 587f won 4 medals in the last SAT Competition 2011 including a gold medal in the parallel application track on multi-core machines for Plingeling.

These are the README and NEWS files of the latest release.

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

These versions of the source code of Lingeling and Plingeling are available under GPL.

For other licenses contact Armin Biere.

Background

Lingeling is a more compact and robust implementation of PrecoSAT with some additional features. Plingeling is a multi-threaded front end implemented with Pthreads. More details can be found in the SAT Race 2010 system description also published as FMV technical report 10/1 and in the SAT Competition 2011 system description which appeared as FMV technical report 11/1.

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 recent papers on SAT mostly focusing on practical SAT solving. On our software page you find earlier SAT solvers and related tools by our group.