Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Pruning Boolean d-DNNF Circuits Through Tseitin-Awareness

Vincent Derkinderen

TL;DR

This work addresses the size blow-up that can occur when converting circuits to CNF via Tseitin transformations, which is common in d-DNNF compilation for tractable weighted model counting. It introduces Tseitin artifacts—tautological subcircuits that emerge after existential quantification of Tseitin variables—and provides a linear-time bottom-up method to detect and prune them, in addition to existentially quantifying Tseitin variables. Empirical results across MCC, CNFT, and neuro-symbolic datasets show large average reductions in circuit size: about 77.5% overall when removing both Tseitin variables and artifacts, with artifact removal contributing an extra 22.2–30.6% depending on the dataset. The findings suggest substantial practical benefits for downstream probabilistic inference tasks and motivate integrating artifact-aware pruning into compilation pipelines to improve efficiency.

Abstract

Boolean circuits in d-DNNF form enable tractable probabilistic inference. However, as a key insight of this work, we show that commonly used d-DNNF compilation approaches introduce irrelevant subcircuits. We call these subcircuits Tseitin artifacts, as they are introduced due to the Tseitin transformation step -- a well-established procedure to transform any circuit into the CNF format required by several d-DNNF knowledge compilers. We discuss how to detect and remove both Tseitin variables and Tseitin artifacts, leading to more succinct circuits. We empirically observe an average size reduction of 77.5% when removing both Tseitin variables and artifacts. The additional pruning of Tseitin artifacts reduces the size by 22.2% on average. This significantly improves downstream tasks that benefit from a more succinct circuit, e.g., probabilistic inference tasks.

Pruning Boolean d-DNNF Circuits Through Tseitin-Awareness

TL;DR

This work addresses the size blow-up that can occur when converting circuits to CNF via Tseitin transformations, which is common in d-DNNF compilation for tractable weighted model counting. It introduces Tseitin artifacts—tautological subcircuits that emerge after existential quantification of Tseitin variables—and provides a linear-time bottom-up method to detect and prune them, in addition to existentially quantifying Tseitin variables. Empirical results across MCC, CNFT, and neuro-symbolic datasets show large average reductions in circuit size: about 77.5% overall when removing both Tseitin variables and artifacts, with artifact removal contributing an extra 22.2–30.6% depending on the dataset. The findings suggest substantial practical benefits for downstream probabilistic inference tasks and motivate integrating artifact-aware pruning into compilation pipelines to improve efficiency.

Abstract

Boolean circuits in d-DNNF form enable tractable probabilistic inference. However, as a key insight of this work, we show that commonly used d-DNNF compilation approaches introduce irrelevant subcircuits. We call these subcircuits Tseitin artifacts, as they are introduced due to the Tseitin transformation step -- a well-established procedure to transform any circuit into the CNF format required by several d-DNNF knowledge compilers. We discuss how to detect and remove both Tseitin variables and Tseitin artifacts, leading to more succinct circuits. We empirically observe an average size reduction of 77.5% when removing both Tseitin variables and artifacts. The additional pruning of Tseitin artifacts reduces the size by 22.2% on average. This significantly improves downstream tasks that benefit from a more succinct circuit, e.g., probabilistic inference tasks.
Paper Structure (25 sections, 1 theorem, 15 equations, 10 figures, 1 table)

This paper contains 25 sections, 1 theorem, 15 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Propositional Logic
  4. Weighted Model Counting
  5. Circuit Properties
  6. CDCL Algorithm
  7. Tseitin Transformation
  8. What are Tseitin Artifacts?
  9. Existential Quantification of Tseitin Variables
  10. Tseitin Artifacts
  11. Detecting Tseitin Artifacts
  12. How To Detect Them?
  13. When Do They Emerge?
  14. Related Work
  15. Experiments
  16. ...and 10 more sections

Key Result

Proposition 1

When $f(\mathbf{X}, \mathbf{Y})$ is a (sub)circuit of a d-DNNF representation for $\mathcal{T}(\psi)$, over Tseitin variables $\mathbf{X}$ and non-Tseitin variables $\mathbf{Y}$, then $f$ is a Tseitin artifact if and only if the unweighted model count is $MC(f) = 2^{|\mathbf{Y}|}$.

Figures (10)

  • Figure 1: A d-DNNF representation of $\mathcal{T}(\psi)$, of Example \ref{['ex:tseitin']}.
  • Figure 2: The d-DNNF of Fig. \ref{['fig:CDCL-full']}, with the Tseitin variables $x_1$ and $x_2$ existentially quantified (that is, $\exists x_1,x_2. \mathcal{T}(\psi)$). The red node indicates the root of a subcircuit that is a Tseitin artifact.
  • Figure 3: The noisy-OR BN where $Prob(pa) = \theta_{pa}$. When $Pa$ is true and its signal is not noisy ($\theta_{pa}^a$), $A$ becomes true.
  • Figure 4: The d-DNNF circuit size for varying sizes of the noisy-OR problem. d-DNNF+p represents $\textsc{EXISTS}(\mathcal{T}(\psi), \mathbf{X})$. d-DNNF+t represents the additional removal of Tseitin artifacts. Lower is better.
  • Figure 5: The fraction of d-DNNF nodes remaining after removing Tseitin artifacts (65 instances of the MCC dataset). Lower is better.
  • ...and 5 more figures

Theorems & Definitions (12)

  • Example 1
  • Definition 1: weighted model count
  • Definition 2: determinism (d)
  • Definition 3: Decomposability (D)
  • Definition 4: Negation Normal Form (NNF)
  • Definition 5: smoothness (s)
  • Example 2
  • Example 3
  • Example 4: Tseitin transformation
  • Definition 6: Tseitin artifact
  • ...and 2 more