Enhancing Query Efficiency for d-DNNF Representations Through Preprocessing

Research Context and Objective

Propositional formulas in Conjunctive Normal Form (CNF) are foundational to automated planning, databases, and explainable AI. However, fundamental tasks such as uniform sampling, direct model access, and model enumeration are computationally expensive (#P-complete). Knowledge compilation into Decision-DNNF (d-DNNF) is a common strategy to make these queries tractable. This paper investigates how preprocessing techniques—typically used to simplify CNF formulas before solving—can be optimized to enhance the efficiency of these specific downstream queries.

Preprocessing and Query Compatibility

The authors categorize preprocessing techniques based on the logical properties they preserve. Techniques that preserve full logical equivalence (e.g., vivification, backbone identification, and occurrence reduction) are universally applicable to all query types. Conversely, techniques that only preserve satisfiability (e.g., variable elimination and blocked clause elimination) are shown to be fundamentally unsuitable for model-related queries, as they destroy the information required to count or sample models accurately.

Leveraging Model-Count Preserving Techniques

A key contribution is the demonstration that techniques preserving model counts—specifically the elimination of implicitly or explicitly defined variables—can be effectively leveraged. While these methods do not preserve logical equivalence, they maintain the total number of models, which is sufficient for direct access and uniform sampling. The authors provide a workflow where these techniques are applied to the CNF formula prior to compilation into d-DNNF. Experimental results on diverse benchmarks confirm that this approach yields significant performance improvements in query runtime without sacrificing the correctness of the results.

This study provides practitioners with a clear roadmap for optimizing logical reasoning pipelines. By identifying which preprocessing techniques are compatible with specific query types, researchers can avoid the pitfalls of using satisfiability-preserving methods for enumeration tasks. The findings emphasize that the choice of preprocessing is not a one-size-fits-all decision but must be aligned with the specific requirements of the downstream inference or sampling task.