sharpSAT

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

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

Building

Prerequisites

• CMake
• GMP (with C++ bindings)

This is a CMake project. To configure a build in the build directory (will be created), run:

cmake -B build

After configuring, build the project with:

cmake --build build

Changes

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