The bn2cnf preprocessor

The bn2cnf translator

bn2cnf is a translator associating with an input graphical model (a Bayesian network or a Markov network) an output which consists of a CNF formula and a weight map. The weight of any piece of evidence for the input model can be computed as the weighted model count of the corresponding output. Several encoding schemes can be considered depending on the options used.

Ressources for the bn2cnf translator (May 2016 version)

For more details, see the paper:

A. Bart, F. Koriche, J.-M. Lagniez, P. Marquis, "An Improved CNF Encoding Scheme for Probabilistic Inference", proceedings of ECAI'16, pages 613-621.

How to use bn2cnf

Let BENCHMARK.uai be a BN instance, which must conform to the UAI competition format (link).

bn2cnf invocation
$ ./bn2cnf -i BENCHMARK.uai [-o outputFile] [-w outputWeightFile] [-v outputMapVariable] [-e typeEncoding] [-implicit] [-s prime]
where:
  • inputFile is the name of the BN file (extension .uai) which must respect the UAI format
  • outputFile is the name of resulting DIMACS format CNF file (default: /dev/stdout)
  • outputWeightFile is the name of the file where the weight map is saved (default: /dev/stdout)
  • outputMapVariable is the name of the file where the variable map is saved (default: /dev/stdout)
  • typeEncoding is a string (LOG or DIRECT) which gives the type of encoding used to represent the variables (default: DIRECT)
  • -implicit means we are going to use the implicit encoding of the most frequent weight
  • -s prime, means we are going to first simplify the CPTs using Quine/McCluskey algorithm
The parameters put into [ ] are optional.

Example

Let us consider the following benchmark 'example.uai' in UAI format (approx. the example given in the paper).

UAI instance
$ cat example.uai
MARKOV
2
3 2
1
2 0 1

6
0 0.26
0.1 0.1
0.26 0.26

The encoding ENC4 (reported in http://reasoning.cs.ucla.edu/fetch.php?id=88&type=pdf) for the given instance can be obtained by running the following command line.

ENC4 encoding
$ ./bn2cnf -i example.uai -o bench.cnf -w weightMap -v varMap -e DIRECT -s prime
c =================== Information about the instance ======================
c Number of CPTs: 1
c Number of tuples for all the CPTs: 6
c Number of variables: 2
c Number of values: 5
c
c =================== Preprocessing (Quine/McCluskey) ==================
c Number of remaining tuples in all CPTs after simplification: 4
c
c =================== Transformation information ======================
c Number of Boolean variables used to encode the domains: 5
c Number of clauses used to encode the domains: 6
c
c =================== CNF information ======================
c Number of variables: 7
c Number of clauses: 10
c
c Total elapsed time: 0.000318
There are five parts in the message:
  • Information about the input instance (the number of tables, the total number of tuples, the number of variables and the total number of values in the domains)
  • Preprocessing (Quine/McCluskey) [optional] (the total number of tuples after simplification)
  • Transformation information (the numbers of variables and clauses used to encode the domains)
  • CNF information (the numbers of variables and clauses in the resulting CNF)
  • The time needed to achieve the encoding (in seconds)

In file varMap, one can find the map associating every elementary assignment over the variables of the input network with the corresponding terms (their propositional encodings):

Variable mappings
$ cat varMap
0 = [[1][2][3]]
1 = [[4][5]]
Each line corresponds to a variable of the input network. At column j we can find the term encoding the elementary assignment associating the jth value of the its domain to this variable.

In file weightMap, one can find the map associating the weights with the literals occurring in bench.cnf.

Weights mapping
$ cat weightMap
6 0.260000
-6 0.740000
7 0.100000
-7 0.900000
0 1.000000
Each line consists of a literal and the corresponding weight. By convention literals not occurring in this map have weight 1. 'Literal' 0 corresponds to the scaling factor.

In file bench.cnf, one can find the resulting CNF formula in DIMACS format.

DIMACS format
$ cat bench.cnf
p cnf 7 10
1 2 3 0
-1 -2 0
-1 -3 0
-2 -3 0
4 5 0
-4 -5 0
-1 -4 0
-1 -5 6 0
-3 6 0
-2 7 0
The first five variables are indicator variables (encoding the assignments) and the last two variables (6 and 7) are parameter variables (encoding the non-null weights occurring in the table). The first six clauses encode the domains and the last four clauses encode the table.
Generated files
$ ./bn2cnf -i example.uai -o bench.cnf -w weightMap -v varMap -e LOG -s prime -implicit

c =================== Information about the instance ======================
c Number of CPTs: 1
c Number of tuples for all the CPTs: 6
c Number of variables: 2
c Number of values: 5
c
c =================== Preprocessing (Quine/McCluskey) ======================
c Number of remaining tuples in all CPTs after simplification: 4
c
c ================= Transformation information - Implicit ==================
c Number of Boolean variables used to encode the domains: 4
c Number of clauses used to encode the domains: 1
c
c =================== CNF information ======================
c Number of variables: 4
c Number of clauses: 3
c
c Total elapsed time: 0.000312
Gives the following content for the generated files:
$ cat varMap
0 = [[1, 2][1, -2][-1, 2]]
1 = [[3][-3]]

$ cat weightMap
4 0.384615
-4 0.615385
0 0.260000

$ cat bench.cnf
p cnf 4 3
1 2 0
-1 -2 -3 0
-1 2 4 0