The B+E preprocessor

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)

For more details, see the paper:

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)

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.

DIMACS CNF formula example
\$ cat ./instance.cnf
c
c this file encodes (a <-> b AND c) AND (a <-> d OR e)
c
p cnf 5 6
-1 2 0
-1 3 0
1 -2 -3 0
-1 4 5 0
1 -4 0
1 -5 0

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.

Example of B+E invocation
\$ B+E ./instance.cnf
c Problem Statistics:
c ...
c
p cnf 5 6
-4 3 0
-4 2 0
-3 5 -2 4 0
3 -5 0
2 -5 0
c The forgotten variables
1 0
c The number of literals is: 12
c The number of variables is: 4

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.

Example of B invocation
\$ B+E -B=inputVars.var ./instance.cnf
c Problem Statistics:
c ...
c

\$cat ./inputVars.var
V 5 4 3 2 0

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).

Example : -limSolver=X
\$ B+E -limSolver=1000 ./instance.cnf
...

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.

Example of E invocation
\$ cat toForget.var
V 1 0

\$ B+E -E=toForget.var ./instance.cnf
c Problem Statistics:
c ...
c

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.

Example : -max#Res=X
\$ B+E -max#Res=1000 ./instance.cnf
...