Version 570 is the latest public release.
Version 570 is the version submitted to the SAT Race 2010 and its successor version 576 is just a maintenance release.
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.
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.
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.