Abstrakt
Knowledge compilation is a process of adding more information to a knowledge base in order to make it easier to deduce facts from the compiled base than from the original one. One type of knowledge compilation occurs when the knowledge in question is represented by a Boolean formula in conjunctive normal form (CNF).
The goal of knowledge compilation in this case is to add clauses to the input CNF until a logically equivalent propagation complete CNF is obtained. A CNF is called propagation complete if after any partial substitution of truth values all logically entailed literals can be inferred from the resulting CNF formula by unit propagation.
The key to this type of knowledge compilation is the ability to generate so-called empowering clauses. A clause is empowering for a CNF if it is an implicate and for some partial substitution of truth values it enlarges the set of entailed literals inferable by unit propagation.
In this paper we study several complexity issues related to empowering implicates, propagation completeness, and its relation to resolution proofs. We show several results: (a) given a CNF and a clause it is co-NP complete to decide whether the clause is an empowering implicate of the CNF, (b) given a CNF it is NP-complete to decide whether there exists an empowering implicate for it and thus it is co-NP complete to decide whether a CNF is propagation complete, and (c) there exist CNFs to which an exponential number of clauses must be added to make them propagation complete.