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.


Authors :
Sébastien Konieczny
Pierre Marquis
Jean-Marie Lagniez

Any category    Compiler   

Go to the software webpage

Book chapters

2017 Sébastien Konieczny, Jean-Marie Lagniez, Pierre Marquis, Boosting Distance-Based Revision Using SAT Encodings in Logic, Rationality, and Interaction, vol. 10455, pp. 480-496, Springer Berlin Heidelberg, 2017.