sharpSAT is a #SAT solver based on modern DPLL based SAT solver technology. This is a new version with several incremental improvements over the 2006 sharpSAT 1.1 which has been published at SAT 2006.
This version also fixed several bugs - most importantly a counting bug, that causes sharpSAT to report wrong model counts on some instances.
Usage: sharpSAT [options] [CNF_File] Options: -noPP turn off preprocessing -noCC turn off component caching -noIBCP turn off implicit BCP -q quiet mode -t [s] set time bound to s seconds -cs [n] set max cache size to n MB
It suffices to change to the ./Release subdirectory and run
make
NOTE:
-
it is necessary to have at least G++ 4.7 installed for sharpSAT to compile. This is particularly necessary as we use delegating constructors
-
the GMP bignum package has to be installed in your system
12.08 <
-
rewrote most of the codebase of the solver, including a redesigned SAT solver foundation based on more recent developments such as MiniSAT and TiniSAT, e.g. conflict clause minimization is used now
-
disentangled component analysis and the SAT solver part by separating the datastructures. Although this imposes a small memory overhead it allows for simpler and faster algorithms both in the SAT solver and in the component analysis part.
-
the redesign reduced the number of code lines by more than 30%
-
implicit BCP is more efficient now since for every failed literal l found every literal corresponding to a UIP of the conflict caused by l is asserted and add a UIP clause for that conflict is added
-
changed the decision heursitics to floating point values, and changed the VSADS weighting and the activity decay rate.
-
As it does not make sense to use only finite precision, the GMP bignumber package is now a prerequisite for sharpSAT. This also has to do with the fact that we use GMP integer arithmetic now instead of GMP floating points which is both simpler and has a small memory advantage.
-
A new coding of the cached components is introduced which frequently saves 30 - 50% of cache memory.
-
reduced the memory overhead of cached components to less than 40% of the original overhead
-
cache size will now be automatically set to at most 95% of the free RAM available at program start. This can be overridden, however, by setting the maximum cache size using the "-cs" option
BUGFIXES
-
corrected a bug in the use of the GMP bignumber package that caused (among others) wrong solution counts reported on bmc-ibm-5, bmc-ibm-10, ra, rb, and rc.
-
the solver is fully 64bit compliant now; esepcially the cache size can now be larger than GB
-
several out-of-memory problems with the old sharpSAT have been resolved