## The br2cnf compiler

### Compilation of a CNF belief revision instance into CNF formula

The br2cnf compiler is a program for compiling a given CNF
belief revision instance into a query-equivalent CNF formula.

Several topic-decomposable distance-based belief revision
operators have been implemented, namely those based on the
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, "Boosting Distance-Based Revision using SAT Encodings", proceedings of LORI'17.

The input instance must respect the following format:

t w1 v1_1 v1_2 ... 0

t w2 v2_1 v2_2 ... 0

....

indicates that #var is the number of variables of the instance, and m is the number of topics. Each line starting with 't' describes a topic. wi is the weight of the ith topic and each vi_j is the jth variable of the ith topic.

are comment lines

Then one can find a number of lines of the form

... 0

... 0

giving the CNF representation (in DIMACS format) of the revision formula.

Follows a number of lines of the form

... 0

... 0

... 0

giving the CNF representation (in DIMACS format) of the initial base.

p cnf 3 4

t 16 1 2 3 0

t 2 1 0

t 4 2 0

t 8 3 0

3 0

1 2 0

s 1

-1 2 0

1 -2 0

-2 -3 0

2 3 0

The options of this command correspond to the 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: br2cnf input-file out-file -d {hamming, drastic} -a {sum, leximin, leximax} -path PATH

- input-file is the file containing the CNF belief revision 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 (drastic or 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)

c Options activated

c distance : hamming

c aggregator: sum

c path : ./maxhs

c

c [ Problem Statistics ]

c Number of variables: 3

c Number of clauses: 6

c Number of bases: 1

c The optimal value found is: 18

c Compilation result in /tmp/beliefRevisionEncoding.cnf

c Compilation time: 0.01

The generated encoding can be found in the file encoding.cnf (it is based on 210 variables and contains 462 clauses); in this encoding, variables 1 to 3 are the same variables as those considered in the input file input.brcnf (hence query-equivalence is ensured on them).