Dynamic Blocked Clause Elimination for Projected Model Counting

TL;DR

This paper introduces a novel approach to apply blocked clause elimination in projected model counting, preserving model counts while improving computational efficiency through new algorithms and data structures.

Contribution

It presents a new method for using blocked clause elimination in projected model counting, including a novel data structure and algorithms, implemented in the d4 model counter.

Findings

Improved efficiency in projected model counting tasks.

Blocked clause elimination can be applied without altering model counts.

Experimental results show computational benefits of the proposed method.

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.{\Sigma}|| of a propositional formula {\Sigma} 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.