[ news | download | license | experiments ]

News

Version 913 is the version used in the SAT'09 SAT Competition.

Version 535 is the first public release.

Download

[ picosat-913.tar.gz | picosat-846.tar.gz | picosat-632.tar.gz | picosat-535.tar.gz ]

Please refer to NEWS for more details.

There are three publications on PicoSAT: a longer article in JSAT and a short paper on controlling restarts. In our FMCAD'08 paper on Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver we describe how PicoSAT has been extended to handle all different constraints symbolically.

Version 535 is the winner in the category of satisfiable industrial instances of the SAT'07 SAT Solver competition, and came second on all industrial instances. The old version 632 is cleaned up and has some more documentation. Also a problem is fixed that occurs when using assumptions incrementally. Please use version 535 for plain speed comparisons and version 632 if you want to use PicoSAT as a library and particularly for incremental applications.

PicoSAT can generate proofs and cores in memory by compressing the proof trace. It supports the proof format of TraceCheck. The library has a simple API which is similar to that of our previous solvers.

License

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

Background

The SAT problem is the classical NP complete problem of searching for a satisfying assignment of a propositional formula in conjunctive normal form (CNF). General information on SAT can be found at www.satlive.org or www.satlib.org. Our invited talk A Short History on SAT Solver Technology and What is Next? describes some of the new features of PicoSAT. The experimental data used in this talk is available as Biere-SAT07-talk-experiments.tar.bz2 (14 MB).