## The bm2cnf compiler

### Compilation of a CNF merging instance into CNF formula

The bm2cnf compiler is a program for compiling a given CNF
merging instance into a query-equivalent CNF formula.

Several distance-based merging operators have been
implemented, namely those based on the (possibly weighted)
drastic distance or Hamming distance between interpretations,
and using sum, leximin or leximax as aggregation function.

For more details, see the paper:

S. Konieczny, J.-M. Lagniez, P. Marquis, "SAT Encodings for Distance-Based Belief Merging Operators", proceedings of AAAI'17, February 4-9, 2017, San Francisco, California, USA., 2017. Pages 1163-1169.

The input instance must respect the extended DIMACS format for CNF merging instances.

The options of this command correspond to the (weighted) distances and the aggregators which have been implemented:

{a, b} means you have to choice between a and b. [c] means that c is optional.

USAGE: bm2cnf input-file out-file -d {hamming, drastic} -a {sum, leximin, leximax} -path PATH

- input-file is the file containing the CNF merging instance (it is given either in plain or in gzipped extended DIMACS format)
- out-file is the name of the file used to save the resulting CNF encoding (out-file.cnf)
- d is the distance used (weighted drastic or weighted Hamming)
- a is the aggregator used (sum, leximin or leximax)
- path gives the path of the solver used to solve the weighted partial maxSAT optimization problem(s)

On the CNF merging instance obtained by using the tt2bm translator, we get (using the Hamming distance and the leximin aggregator, and the maxhs software as SAT-based optimizer):

c Options activated

c distance : hamming

c aggregator: leximin

c path : ./maxhs

c

c [ Problem Statistics ]

c Number of variables: 96

c Number of clauses: 232

c Number of bases: 3

c run: (score, #base)

c 0: ( 1, 49)

c 1: ( 2, 33)

c 2: ( 3, 49)

c Encoding generated in encoding.cnf

c Compilation time: 0.01

The information displayed make precise first the number of
variables (96), the number of clauses (232), and the number
of bases (3) in the input merging instance. Then one can
find the value of the distance between the integrity
constraint and the profile, given here as a list of pairs
since the leximin aggregator has been used. This distance is
1 (repeated 49 times), then 2 (repeated 33 times) followed
by 3 (repeated 49 times). The repetitions reflect the weights
of the bases (note that such weights have no impact on the merged base
when the aggregator is leximax
or leximin). encoding (.cnf) is the name of
the output file, containing the CNF encoding which has been
generated, and compilation time makes precise the time (in
seconds) needed to generate this encoding.

Finally, the generated encoding can be found in the
file encoding.cnf (it
is based on 1968 variables and contains 4038 clauses); in
this encoding, variables 1 to 96 are the same variables as
those considered in the input
file merging.cnfs
(hence query-equivalence is ensured on them).