This is a modified version of SharpSAT-TD that can compile CNFs into sd-DNNFs. Use with
./sharpSAT -dDNNF -decot 1 -decow 100 -tmpdir . -cs 3500 in.cnf -dDNNF_out out.nnf
to compile the cnf in.cnfinto an sd-DNNF saved in the file out.cnf. Without -dDNNF_out the sd-DNNF is printed to stdout.
For this to work, the input CNF must have weight annotations of the form
c p weight <lit> <lit> 0
for each literal 0 < abs(lit) <= #vars.
Submission to model counting competition 2021 by Tuukka Korhonen and Matti Järvisalo (University of Helsinki). SharpSAT-TD is based on SharpSAT, with the main new features being the use of tree decompositions in decision heuristics, new preprocessor, and directly supporting weighted model counting.
SharpSAT-TD supports exact model counting, exact weighted model counting with arbitrary precision floats, and exact weighted model counting with doubles. See a detailed description in description.pdf.
The external dependencies needed are the GMP library, the MPFR library, and CMAKE.
To compile and link dynamically use
./setupdev.sh
To compile and link statically use
./setupdev.sh static
The binaries sharpSAT and flow_cutter_pace17 will be copied to the bin/ directory.
The currently supported input/output formats are those of Model counting competition 2021.
Example unweighted model counting:
cd bin
./sharpSAT -decot 1 -decow 100 -tmpdir . -cs 3500 ../examples/track1_009.cnf
Example weighted model counting with arbitrary precision:
cd bin
./sharpSAT -WE -decot 1 -decow 100 -tmpdir . -cs 3500 -prec 20 ../examples/track2_003.wcnf
Example weighted model counting with double precision:
cd bin
./sharpSAT -WD -decot 1 -decow 100 -tmpdir . -cs 3500 ../examples/track2_003.wcnf
In the competition setting the value of the -decot flag was 120.
-decot- the number of seconds to run flowcutter to find a tree decomposition. Required. Recommended value 60-600 if running with a total time budjet of 1800-3600 seconds.-tpmdir- the directory to store temporary files for running flowcutter. Required.-decow- the weight of the tree decomposition in the decision heuristic. Recommended value >1 if the heuristic should care about the tree decomposition.-cs- limit of the cache size. If the memory upper bound is X megabytes, then the value here should be around x/2-500.-WE- enable weighted model counting with arbitrary precision.-WD- enable weighted model counting with double precision.-prec- the number of digits in output of weighted model counting. Does not affect the internal precision.