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) andO
(output), such that for every instantiation of all the variables ofI
satisfying the input CNF formula, every variable inO
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.
...