$ 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
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:
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:
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
- 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)
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).