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.

Any category    Compiler   

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.