On Lower Bounding Minimal Model Count

TL;DR

This paper introduces two novel techniques using answer set programming to establish lower bounds on the number of minimal models of Boolean formulas, improving estimation accuracy and runtime efficiency.

Contribution

It presents new methods for counting minimal models by combining knowledge compilation and hashing-based approximate counting, advancing quantitative analysis in this area.

Findings

Significantly improved lower bound estimates for minimal models.

Enhanced runtime performance over existing reasoning systems.

Effective application of answer set programming techniques.

Abstract

Minimal models of a Boolean formula play a pivotal role in various reasoning tasks. While previous research has primarily focused on qualitative analysis over minimal models; our study concentrates on the quantitative aspect, specifically counting of minimal models. Exact counting of minimal models is strictly harder than #P, prompting our investigation into establishing a lower bound for their quantity, which is often useful in related applications. In this paper, we introduce two novel techniques for counting minimal models, leveraging the expressive power of answer set programming: the first technique employs methods from knowledge compilation, while the second one draws on recent advancements in hashing-based approximate model counting. Through empirical evaluations, we demonstrate that our methods significantly improve the lower bound estimates of the number of minimal models, surpassing the performance of existing minimal model reasoning systems in terms of runtime.