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

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

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:

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

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.

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

`-limSolver=X`

...

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.

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.

...