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, to appear.

The input instance must respect the following format:

p cnf #var m
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.

c ...

are comment lines

Then one can find a number of lines of the form

... 0
... 0
... 0

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

Follows a number of lines of the form

s 1
... 0
... 0
... 0

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

Example of belief revision instance:
$ cat input.brcnf
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
In order to turn a CNF belief revision instance into a query-equivalent output CNF formula, use:
$ ./br2cnf

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

To get some help:
$ ./br2cnf -help
{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

Compilation of a CNF belief revision instance:
$ ./br2cnf input.brcnf beliefRevisionEncoding -d hamming -a leximin -path ./maxhs
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).

Addition ressources:
Empirical results: table
Benchmarks: here
Belief revision benchmark generator: in progress