Projected Model Counting and Enumeration

Model counting is the problem of calculating the number of truth assignments (or models) satisfying a given propositional formula (typically represented as a CNF). While SAT solving is known to be one of famous NP-complete problems, model couting is known to be #P-complete.

Our research focus is projected model counting and enumeration. In projected model counting, given a propositional formula F and a subset P of variables (called projection variables), we count models of F with respect to P. We are developing solvers for projected model counting and enumeration.

GPMC
PC2BDD

GPMC

GPMC is an exact projected model counter for CNF formulas.

Download

Git repository
version for Model Counting Competition 2022 (1st place in Track3(PMC) at MC2022)
version for Rep-Tile benchmark (Experimental)

Publications

[SHS17] Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai,
Improvement of Projected Model-Counting Solver with Component Decomposition Using SAT Solving in Components,
JSAI Technical Report, SIG-FPAI-103-B506, pp. 31-36, Mar 2017 (in Japanese).
[SKM15] Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai,
An Extension of a DPLL-Based Model-Counting Solver for Projected Model,
JSAI Technical Report, SIG-FPAI-97-B404, pp. 59-64, Mar 2015 (in Japanese).

PC2BDD

PC2BDD constructs a BDD which represents a set of projected models for a CNF formula and a set of projection variables.

Download

source code on gitlab
version for Model Counting Competition 2021 (4th place in Track3(PMC) at MC2021)

Publications

[IHS21] Takaaki Isogai, Kenji Hashimoto, and Masahiko Sakai,
A Method of BDD Construction to Represent All Projected Models of a Propositional Logic Formula,
JSAI Technical Report, SIG-FPAI-116, pp. 14-19, Mar 2021 (in Japanese).

Benchmark

OPT-SMALLINT-LIN-NaPS [5.5GB]
- generated by NaPS 1.02b from opb instances of PB Competition 2016, OPT-SMALLINT-LIN category
Filelist of a subset of OPT-SMALLINT-LIN-NaPS (571 instances) for pc2bdd, used in [IHS21]

Last modified: Sep.15.2021.