Abstract
Propagation complete formulas were introduced by Bordeaux and Marques-Silva (2012) as a possible target language for knowledge compilation. A CNF formula is propagation complete (PC) if for every partial assignment, the implied literals can be derived by unit propagation.
Bordeaux and Marques-Silva (2012) proposed an algorithm for compiling a CNF formula into an equivalent PC formula which is based on incremental addition of so-called empowering implicates. In this paper, we propose a compilation algorithm based on the implicational structure of propagation complete formulas described by Kucera and Savicky (2020) and the algorithm for learning a definite Horn formula with closure and equivalence queries introduced by Atserias et al. (2021).
We have implemented both approaches and compared them experimentally. Babka et al. (2013) showed that checking if a CNF formula admits an empowering implicate is an NP-complete problem.
We propose a particular CNF encoding which allows us to use a SAT solver to check propagation completeness, or to find an empowering implicate.