[  news | download | old-versions | license | experiments | resources ]

News

New release 965, see NEWS.

Download

[ picosat-965.tar.gz ]

[ checkmus ]

With release 965 we support inclusion of PicoSAT into R projects thanks to Christoph M¨ssel (see BoolNet), which also led to more clean code related to the usage of pointer differences. The all-difference-constraint code was partially revived (thanks to Himanshu Jain). We also added support for our new generic incremental SAT solver interface ipasir.h as used in the incremental track of the last SAT Race'15.

Version 960 fixes severals issues found by Stefan Hengelein. and version 957 contains several fixes for bugs in 'picosat_deref_partial' reported by Rüdiger Ehlers.

Version 953 became reentrant. This allows multiple PicoSAT instances in the same process. This changes most of API functions which now require an additional PicoSAT manager object as first argument. In version 954 we define the macro PICOSAT_REENTRANT_API in the header file. The previous release 951 is a cleaned-up version after incorporating comments by Donald Knuth.

For more details refer to NEWS and to the SAT Race 2010 system description also published as FMV technical report 10/1.

The API is described in a tutorial talk on Using High Performance SAT and QBF Solvers, (tptpa11satdemo.zip) as part of Theorem Proving Tools for Program Analysis (TPTPA'11), a Tutorial which was co-located with POPL'11. The header file picosat.h has substantial documentation as well.

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.

Please use the PicoSAT article for citations.

PicoSAT can generate proofs and cores in memory by compressing the proof trace. It supports the proof format of TraceCheck.

Old Versions

[ picosat-960.tar.gz ]
[ picosat-959.tar.gz ]
[ picosat-957.tar.gz ]
[ picosat-954.tar.gz ]
[ picosat-953.tar.gz ]
[ picosat-951.tar.gz ]
[ picosat-936.tar.gz ]
[ picosat-913.tar.gz ]
[ picosat-846.tar.gz ]
[ picosat-632.tar.gz ]
[ picosat-535.tar.gz ]

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.cs.ubc.ca/~hoos/SATLIB. 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).

Other Resources

PycoSAT python bindings for PicoSAT by Ilan Schnell.

PyEDA with PicoSAT bindings by Chris Drake.

PiGoSAT Go bindings for PicoSAT by William Schwartz.