Compile! Project - CRIL-CNRS & Univ. Artois

B+E: Improving Model Counting by Leveraging Definability

B+E is a preprocessor that associates with an input CNF an output CNF which admits the same number of models. B+E tracks definability relations between variables (aka gates) and use them to reduce the instance by eliminating variables which have been identified as outputs of some gates.

Ressources for the B+E preprocessor (April 2016 version)

• the runtime code of our preprocessor B+E under GNU/Linux and Mac OS operating systems
• a list of the benchmarks considered in our experiments
• the benchmarks themselves
• a spreadsheet file synthesizing the empirical results

Source code

The source code can be found on Github.

For more details, see the papers:

J.-M. Lagniez, E. Lonca, P. Marquis. "Improving Model Counting by Leveraging Definability". Proceedings of IJCAI'16, pages 751-757. (link to full proof version)

J.-M. Lagniez, E. Lonca, P. Marquis. "Definability for model counting.". Artificial Intelligence, vol. 281. (link to sciencedirect.com)

How to use B+E

Let instance.cnf be a CNF instance, which must conform to the standard DIMACS format. As an example, the following file encodes a CNF formula.

B+E proceeds in two steps:

1. B, which stands for "Bipartition", splits the variables into two disjoint sets I (input) and O (output), such that for every instantiation of all the variables of I satisfying the input CNF formula, every variable in O has a unique truth value in this formula;
2. E, which stands for "Elimination", tries to reduce the size of the input CNF formula by forgetting some variables of O using the resolution rule.

An invocation of B+E with an input cnf file as its unique argument results in applying successively the two steps on the input formula, and generates a CNF formula having the same number of model as the input formula.

Both steps can be applied separately. Using -B=inputVars.var launches the bipartition algorithm and stores the variables of I in the file inputVars.vars. This file is composed of a single line, starting with the V character followed by the input variables, each of them being preceeded by the space character.

B is a greedy algorithm, trying to get a set O which is quite large. However, only the maximality od O w.r.t. set inclusion is guaranteed. In order to keep to computation time to stay small, the number of conflicts allowed for the integrated SAT oracle to determine whether a variable may be defined from the current I set is bounded. This limit may be set using the option -limSolver=X where X is the number of allowed conflicts (0 for infinity, default value).

In order to use E alone, the option E=toForget.var must be used. In this case, the elimination process is applied on the formula, but focusing only on the variables in toForget.var. This file has the same format as the one generated when invoking B+E with the -B option, and must involve variables of the formula, only.

E may also be tuned using the max#Res=X option, which bounds the number of generated resolvents when a variable is forgetten; if this bound is exceeded, then the forgetting process is aborted. Default value is 500.