PrecoSAT

News

Version 570 is the latest public release.

Download

[ precosat-576-7e5e66f-120112.tar.gz | precosat-570-239dbbe-100801.tar.gz ]

Version 570 is the version submitted to the SAT Race 2010 and its successor version 576 is just a maintenance release.

More details can be found in the SAT Race 2010 system description also published as FMV technical report 10/1.

Version 465 is the first version with an implementation of blocked clause elimination (BCE) described in our TACAS'10 paper.

The second release of the 465 branch fixes a problem in handling blocked clauses through the API.

Version 236 won the gold medal in the applications category of the last SAT Competition. It also won silver medals both for satisfiable instances only and for unsatisfiable instances only again in the applications track.

License

PrecoSAT uses an MIT style license. In essence, you can use and modify the sources as you like provided that you acknowledge the origin of the software in the source code. More details can be found in the LICENSE file that comes with the sources. There is no warranty.

Background

The ideas behind PrecoSAT are partially described in the system description for the SAT'09 SAT Competition.

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 for the field.

Further information on SAT can be found at www.cs.ubc.ca/~hoos/SATLIB. 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.

Older Versions

[ precosat-570-239dbbe-100801.tar.gz | precosat-465r2-2ce82ba-100514.tar.gz | precosat-465-02807a3-100208.tar.gz | precosat236.zip ]