Lingeling and Plingeling
New source code release version ala.
SAT Competition 2011 version 587f released.
Version 276 was the first public release.
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 last 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.
These versions of the source code of Lingeling and Plingeling are available under GPL.
For other licenses contact Armin Biere.
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.