Compile! Project - CRIL-CNRS & Univ. Artois

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.

In order to turn a CNF merging instance into a query-equivalent output CNF formula, use:

$ ./bm2cnf

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

To get some help:

$ ./bm2cnf -help
{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):

Compilation of a CNF merging instance:

$ ./bm2cnf merging.cnfs encoding -d hamming -a leximin -path ./maxhs
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).