Minimal Model Counting via Knowledge Compilation
Mohimenul Kabir
TL;DR
This work addresses counting minimal models of propositional CNF formulas by introducing KC-min, a top-down knowledge compiler that uses a pair representation (P,Q) with P = F ∧ Forced(F) and Q = Copy(F). It provides Forced(F) to over-approximate minimal models, Copy(F) to handle cyclic structures via copy variables, and mechanisms for decomposition, determinism, and justification-based base-case checks to compute $\mathsf{CntMM}(F)$. Theoretical guarantees are given through three lemmas ensuring justification, decomposition, and determinism yield correct counts, with acyclic inputs folding into $\#\mathsf{P}$ complexity and cyclic inputs handled via SAT-based justification. The results pave the way for a dedicated minimal-model counting compiler with potential practical impact on tasks like circumscription and diagnosis, while highlighting future work on implementation and scalability.
Abstract
Counting the number of models of a Boolean formula is a fundamental problem in artificial intelligence and reasoning. Minimal models of a Boolean formula are critical in various reasoning systems, making the counting of minimal models essential for detailed inference tasks. Existing research primarily focused on decision problems related to minimal models. In this work, we extend beyond decision problems to address the challenge of counting minimal models. Specifically, we propose a novel knowledge compilation form that facilitates the efficient counting of minimal models. Our approach leverages the idea of justification and incorporates theories from answer set counting.