Propositional lower bounds: Algorithms and complexity

Propositional greatest lower bounds (GLBs) are logically-defined approximations of a knowledge base. They were defined in the context of Knowledge Compilation, a technique developed for addressing high computational cost of logical inference. A GLB allows for polynomial-time complete on-line reasoning, although soundness is not guaranteed. In this paper we propose new algorithms for the generation of a GLB. Furthermore, we give precise characterization of the computational complexity of the problem of generating such lower bounds, thus addressing in a formal way the question "how many queries are needed to amortize the overhead of compilation?"