GPMC

This is an extension of the original GPMC code, to support complex numbers. To do that a Complex MPFR class has been defined in the files c-mpfr/ComplexMPFR.cc and c-mpfr/ComplexMPFR.h. In addition, the core/Instance.cc and core/Instance.h files have been adjusted to support reading complex weights and to core/Main.cc to print the complex numbers and increase the precision. Lastly, small modifications have been made to include and instantiate templates with the Complex MPFR class.

GPMC is an exact model counter for CNF formulas. The current version of GPMC supports model counting, weighted model counting, projected model counting, and weighted projected model counting.

The source codes of this software are based on those of MiniSat-based Sat solver Glucose 3.0 and SharpSAT 12.08.1. And also, inspired by sharpSAT-TD, the current version incorporates a preprocessor for simplifying input formulas, and uses tree decomposition in decision heuristics. In the implementation, we use a part of source files of the preprocessor in sharpSAT-TD, and use FlowCutter for tree decomposition.

Installation

See INSTALL.md.

Usage

$ ./gpmc [options] [file]

Options:

• -mode=<0..3>

  • 0 : Model Counting
  • 1 : Weighted Model Counting
  • 2 : Projected Model Counting
  • 3 : Weighted Projected Model Counting

• -ddnnf / -no-ddnnf
  construct a d-DNNF with a variable mapping (default: off).
  The d-DNNF is for the CNF simplified by the preprocessor.
  The information about the correspondence between the input and simplified CNF is maintained.

• -nnfout=<string>
  write a constructed d-DNNF to the specified file when -ddnnf is set (default: no file output). The variable correpondance

• -natw / -no-natw
  use mpz_class as the internal data type for weights when weighted model counting (default: off, use mpfr::mpreal).
  Note that we must give natual number weights for each literals in an input file (like "c p weight 1 2 0").

• -prec=<1..intmax>
  set the precision of floating-point numbers (default: 15).

• -cs=<1..intmax>
  set maximum component cache size (MB) (default: 4000)
  NOTE: This bound is only for component cache. GPMC may use much more memory.

Input file format

Input boolean formulas should be in DIMACS CNF format, together with additional information, weights and projection variables. GPMC supports the MCC2021 format.

Example:

p cnf 3 4
c p show 2 3 0
c p weight 2 -1 -3 0
c p weight -2 0.4 0
-1 2 0
-2 3 0
2 -3 0
1 -2 3 0

The set of projection variables is { 2, 3 }. The weight of the positive literal of var 2 is -1-3i, and that of the negative one is 0.4.

Original Author

Kenji Hashimoto, Nagoya University, Japan.