The sharpSAT #SAT solver

sharpSAT is a program that solves the #SAT problem. That is, given a propositional formula F in CNF, #SAT asks for the number of satisfying assignments of F. Like the #SAT solver Cachet, it is based on the famous DPLL algorithm and several techniques that originated in SAT solving.

The most recent version - currently the August 2012 Release - of sharpSAT is available for download here. This new version offers significant speed-ups over previous versions of sharpSAT as can been seen on the benchmark page.  If you are interested in the development of sharpSAT check out its GitHub repository which provides, among other things, several unstable development versions. 


February 4, 2013 A bug fix release is available resolving an issue pointed out and fixed by Vladmir Klebanov.

August 28, 2012 New Release of sharpSAT available on GitHub. The changes include (more details)
  • a rewritten codebase of the solver which results in 30% less lines of code. A redesigned SAT solver foundation based on more recent developments such as MiniSAT and TiniSAT offering e.g. conflict clause minimization
  • changes in the decision heuristic which adapt more quickly to the existence / absence of conflicts
  • more efficient implicit BCP
  • a new coding scheme for the component cache which frequently saves 30 - 50% of cache memory.
  • removed a bug which lead to wrong model counts in earlier versions of sharpSAT
  • several out-of-memory problems have been resolved
  • the solver is now fully 64bit compliant, allowing, for example, cache sizes beyond 4GB.
December 4, 2007 bugfix for a compilation problem on some 64 bit systems.
July 25, 2006 the source code of sharpSAT 1.1 is available.
April 04, 2006 the source code of sharpSAT 1.0 is available


previous versions of sharpSAT are still available here.

Papers on sharpSAT

Other #SAT solvers

  • Cachet - introduced several techniques used in sharpSAT.
  • relsat - a precursor for both Cachet and sharpSAT.

  • c2d - this solver is significantly different from sharpSAT.  While frequently slower, it can solve some of the instances which are very hard for sharpSAT quite easily.