Compile! Project - CRIL-CNRS & Univ. Artois

projMC is a recursive algorithm for projected model counting, i.e., the problem consisting in determining the number of models ||∃X.Σ|| of a propositional CNF formula Σ after eliminating from it a given set X of variables. Based on a ”standard” model counter, our algorithm takes advantage of a disjunctive decomposition scheme of ∃X.Σ for computing ||∃X.Σ||. It also looks for disjoint components in its input for improving the computation.

For more details, see the paper:

J.-M. Lagniez and P. Marquis, "A Recursive Algorithm for Projected Model Counting". Proceedings of AAAI'19.

Ressources for the projected model counter projMC

• the runtime code of projMC under Linux OS
• the benchmarks considered in the experiments (folder "benchmarks"); this folder contains three subfolders corresponding to the three families of instances taken into account (randomBenchs, circuitBenchs, planningBenchs)
• a spreadsheet describing the empirical results (results.ods). It contains five sheets (one per projected model counter used in the experiments). Every sheet has three columns. The first one characterizes the benchmark under consideration (the format is name_nameVar, where name.cnf is the name of the CNF part of the instance and nameVar.var contains the variables of name.cnf to be kept). The second column indicates whether the instance has been solved or a time-out occurred. The third column gives the time (in seconds) needed by projMC to solve the instance ("-" when it has not been solved).

How to use projMC:

Let name.cnf be the input CNF instance (it conforms to the standard DIMACS format).

Associated with it (in the same folder) can be a file name_nbvar.var which contains the list of variables occurring in name.cnf which must be kept (i.e., all the other variables of name.cnf must be forgotten). name_nbvar.var simply contains variable identifiers (positive integers) separated by commas. nbvar denotes an integer which gives the number of variables to be kept. If the option -fpv="name_nbvar.var" is not used, then projMC counts the number of models of name.cnf.

To launch projMC on name.cnf given the variables to be kept in name_nbvar.cnf, run ./projMC name.cnf -fpv=“name_nbvar.var"

Some messages are then reported in the standard output. The first group of lines are about the benchmark itself (they make precise successively its number of variables, its number of clauses, and its size in number of literals). Integer mode is the default mode (used for unweighted model counting).

The second group recalls the default options used by the underlying model counter (D4).

Then some statistics are provided about the solving of the instance. A first group of lines synthesizes some data about the “standard” model counting task (number of calls to the model counter, number of decomposable AND nodes found, number of decision nodes generated). A second group of lines synthesizes some data which are specific to the projected model counting task (number of calls to the projected model counter, number of decomposable AND nodes found, number of UNSAT subproblems found, number of positive hits in the cache).

Finally, the time (in seconds) needed to count the number of models of name.cnf, once projected on the set of variables specified by name_nbvar.var is reported.

Here is an example of invocation of projMC, where the input CNF benchmark is stored in the file circ_30_1.cnf of the circuitBenchs subfolder. The 94 variables to be kept are reported in the file circ_30_1_94.var located in the same subfolder. The messages written in the standard output are:

Thus the time needed by projMC to solve this instance is 0.029554s and the corresponding projected model count is 549957444 models.