Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamic Blocked Clause Elimination for Projected Model Counting

Jean-Marie Lagniez, Pierre Marquis, Armin Biere

TL;DR

This work tackles projected model counting by adapting blocked clause elimination (BCE) to preserve the projected count when eliminating variables. It introduces a dynamic, in-processing BCE framework built around a BlockedClauseManager that leverages a watched-literal–inspired mechanism to identify and remove BCE-friendly clauses at each decision level, all integrated into a DPLL-based counter $d4$. Theoretical insights show that removing BCE-blocked clauses on projected variables preserves the existentially quantified semantics, enabling safe simplification during search. Empirically, dynamic BCE (d4_i) improves solving performance across MC competition benchmarks, solving more instances and achieving substantial time savings compared to baseline and preprocessing-only variants. The results underscore the practical value of BCE in projected model counting and point to promising future enhancements such as RAT/PR-based reductions and broader applicability to related reasoning tasks.

Abstract

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ||\exists X.Σ|| of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

Dynamic Blocked Clause Elimination for Projected Model Counting

TL;DR

This work tackles projected model counting by adapting blocked clause elimination (BCE) to preserve the projected count when eliminating variables. It introduces a dynamic, in-processing BCE framework built around a BlockedClauseManager that leverages a watched-literal–inspired mechanism to identify and remove BCE-friendly clauses at each decision level, all integrated into a DPLL-based counter . Theoretical insights show that removing BCE-blocked clauses on projected variables preserves the existentially quantified semantics, enabling safe simplification during search. Empirically, dynamic BCE (d4_i) improves solving performance across MC competition benchmarks, solving more instances and achieving substantial time savings compared to baseline and preprocessing-only variants. The results underscore the practical value of BCE in projected model counting and point to promising future enhancements such as RAT/PR-based reductions and broader applicability to related reasoning tasks.

Abstract

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ||\exists X.Σ|| of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.
Paper Structure (7 sections, 2 theorems, 1 figure, 1 table, 7 algorithms)

This paper contains 7 sections, 2 theorems, 1 figure, 1 table, 7 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Blocked Clause Elimination for Projected Model Counting
  4. Theoretical Insights
  5. Implementation Details
  6. Experimental Evaluation
  7. Conclusion and Perspectives

Key Result

Proposition 7

Let $\exists x . \Sigma$ be an existentially quantified CNF formula. If a non-tautological clause $\alpha \in \Sigma$ is blocked by a literal $\ell \in \alpha$ with $Var(\ell) = x$, then $\exists x . \Sigma$ is logically equivalent to $\exists x . \Sigma'$, where $\Sigma' = \Sigma \setminus \{\alph

Figures (1)

  • Figure 1: Experimental results

Theorems & Definitions (13)

  • Example 1
  • Example 2: Example \ref{['ex:running']} cont'd
  • Example 3: Example \ref{['ex:running']} cont'd
  • Example 4: Example \ref{['ex:running']} cont'd
  • Example 5: Example \ref{['ex:running']} cont'd
  • Example 6: Example \ref{['ex:running']} cont'd
  • Proposition 7
  • Corollary 8
  • Example 9: Example \ref{['ex:running']} cont'd
  • Example 10: Example \ref{['ex:running']} cont'd
  • ...and 3 more