Dynamic Blocked Clause Elimination for Projected Model Counting
This work addresses a specific problem in automated reasoning for projected model counting, representing an incremental improvement over existing methods.
The paper tackles the challenge of applying blocked clause elimination to projected model counting without altering the model count, by focusing on projected variables during the search. The result is a novel data structure and algorithms implemented in the model counter d4, showing computational benefits in experiments.
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.