SAT Preprocessor
 SAT Solver
 #SAT Solver
 PB / MaxSAT
 Solver Evaluation

The CDCL based model counter sharpCDCL

Author: Norbert Manthey   |   Most recent publication   |   Download source code  

The framework uses Minisat (the version maintained at github, February 2013), and extends this solver with model counting, projection and by combining these two methods the tool can also transform the formula from CNF into DNF.

Usage of the model counter

In this section a brief overview of the usage for the solver is given to enable a quick and easy start with the tool.


How to get the solver? Follow this link download and extract the tar ball.


How to use the tool for solving SAT? To run the solver type ./sharpCDCL INSTANCE, the usual minisat solver will be executed.


Can I use parameters? To list available parameters, type ./sharpCDCL --help


How to count all models? Run ./sharpCDCL -no-pre -countMode=1 INSTANCE (can count at most 2G models)


How to check whether a formula has more than one model? Run ./sharpCDCL -no-pre -maxModel=2 -countMode=1 INSTANCE


How can models with projection be generated? Run ./sharpCDCL -countMode=2 -projection=scope.var INSTANCE . The file scope.var contains all variables that are inside the projection scope, each on a separage line. Note, that sharpCDCL will use the preprocessor by default, without damaging the outcome of the formula.

How can a DNF be compiled? Run ./sharpCDCL -no-pre -countMode=1 -projectToDNF=instance.dnf INSTANCE . After success (might take quite some time because all models need to be enumerated) the file instance.dnf will contain a set of dual clauses that describe the input instance.

How can a DNF be compiled, that uses the projection scope? Run ./sharpCDCL -countMode=2 -projection=scope.var -projectToDNF=instance.dnf INSTANCE . The file scope.var contains all variables that are inside the projection scope, each on a separage line. After success (might take quite some time because all models need to be enumerated) the file instance.dnf will contain a set of dual clauses that describe the input instance with respect to the projection scope. Note, that sharpCDCL will use the preprocessor by default, without damaging the resulting DNF formula.


ICCL Home   |   Institute of Artificial Intelligence - KRR Group   |   Publications