Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Lower Bounding Minimal Model Count

Mohimenul Kabir, Kuldeep S Meel

TL;DR

This work addresses the problem of counting minimal models of a propositional formula, a task known to be $\#\mathsf{co}$-$\mathsf{NP}$-hard, by developing two ASP-based techniques to derive lower bounds on $|\mathsf{MinModels}(F)|$. The first method leverages knowledge-compile-inspired formula decomposition and justified assignments to enable projected enumeration, while the second uses hashing-based approximate counting with independent supports. A hybrid solver, MinLB, selects between these strategies based on decomposability to provide reliable lower bounds with probabilistic guarantees. Empirical results on model-counting benchmarks and itemset-mining generators show that these methods yield stronger lower bounds and competitive runtimes compared to existing minimal-model reasoning systems, enabling scalable assessment of feasibility for full enumeration.

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.

On Lower Bounding Minimal Model Count

TL;DR

This work addresses the problem of counting minimal models of a propositional formula, a task known to be --hard, by developing two ASP-based techniques to derive lower bounds on . The first method leverages knowledge-compile-inspired formula decomposition and justified assignments to enable projected enumeration, while the second uses hashing-based approximate counting with independent supports. A hybrid solver, MinLB, selects between these strategies based on decomposability to provide reliable lower bounds with probabilistic guarantees. Empirical results on model-counting benchmarks and itemset-mining generators show that these methods yield stronger lower bounds and competitive runtimes compared to existing minimal-model reasoning systems, enabling scalable assessment of feasibility for full enumeration.

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.
Paper Structure (34 sections, 7 theorems, 6 equations, 4 figures, 2 tables, 3 algorithms)

This paper contains 34 sections, 7 theorems, 6 equations, 4 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Propositional Satisfiability.
  4. Answer Set Programming.
  5. From Minimal Models to Answer Sets.
  6. Approximate Lower Bound.
  7. Minimal Generator in Itemset Mining.
  8. Encoding Minimal Generators as Minimal Models.
  9. Related Works
  10. Estimating the Number of Minimal Models
  11. Formula Decomposition and Minimal Model Counting
  12. Formula Decomposition by "Cut"
  13. Challenges in Knowledge Compilation for Counting Minimal Models
  14. Minimal Model Counting using Justified Assignment
  15. Algorithm: Counting Minimal Models by Projected Enumeration
  16. ...and 19 more sections

Key Result

Lemma 1

Given a transaction database $D$, $\sigma$ is a minimal model of $\mathsf{MG}(D)$ if and only if the corresponding itemset $I_{\sigma} = \{a | p_a \in \sigma\}$ is a minimal generator of $D$.

Figures (4)

  • Figure 1: The lower bound of $\mathsf{Proj\text{-}Enum}$ and $\mathsf{HashCount}$ vis-a-vis the lower bound returned by clingo on minimal model counting benchmark. The axes are in log scale.
  • Figure 2: The lower bound returned by $\mathsf{Proj\text{-}Enum}$ and $\mathsf{HashCount}$ vis-a-vis the lower bound given by clingo on minimal generators benchmark. The axes are in log scale.
  • Figure 3: The lower bounds returned by $\mathsf{Proj\text{-}Enum}$, $\mathsf{HashCount}$, and existing minimal model counting tools. The $y$-axis show the log of the number of models.
  • Figure 4: The relative quality of $\mathsf{Proj\text{-}Enum}$ and $\mathsf{HashCount}$ vis-a-vis different cut and independent support size, where clingo is used as the reference baseline. The horizontal line is drawn across $r = 1$.

Theorems & Definitions (15)

  • Lemma 1
  • Example 1
  • Lemma 2
  • Theorem 1
  • proof
  • Lemma 3
  • proof
  • proof
  • Lemma 4
  • proof
  • ...and 5 more