Learning to Reason: Leveraging Neural Networks for Approximate DNF Counting

TL;DR

This paper introduces a neural network-based method for approximate weighted DNF counting that achieves linear-time performance for bounded-width formulas, demonstrating strong generalization on large instances.

Contribution

It presents a novel neural model counting approach that combines deep learning with approximate model counting for weighted #DNF, achieving scalable and accurate results.

Findings

Achieves linear-time approximation for bounded-width weighted #DNF

Model generalizes well to large-scale instances

Outperforms traditional methods in scalability and accuracy

Abstract

Weighted model counting (WMC) has emerged as a prevalent approach for probabilistic inference. In its most general form, WMC is #P-hard. Weighted DNF counting (weighted #DNF) is a special case, where approximations with probabilistic guarantees are obtained in O(nm), where n denotes the number of variables, and m the number of clauses of the input DNF, but this is not scalable in practice. In this paper, we propose a neural model counting approach for weighted #DNF that combines approximate model counting with deep learning, and accurately approximates model counts in linear time when width is bounded. We conduct experiments to validate our method, and show that our model learns and generalizes very well to large-scale #DNF instances.

Tables

Table 1. Table 1: Distribution of formula sizes in the training set.

Size ($n$)	50	100	250	500
Count	30000	20000	16000	12000
Size ($n$)	750	1000	2500	5000
Count	10000	8000	6000	3000

Table 2. Table 2: GNN accuracy (%) w.r.t. to additive thresholds.

Evaluation Data	Thresholds
	0.02	0.05	0.10	0.15
Training Set	87.14	98.80	99.97	99.99
Test Set	87.37	98.76	99.95	99.98

Table 3. Table 3: GNN accuracy (%) over test set by threshold versus number of formula variables ( n 𝑛 n ).

$n$	Thresholds
	0.02	0.05	0.10	0.15
50	85.58	98.58	99.98	100.0
100	87.87	98.87	100.0	100.0
250	87.93	99.24	100.0	100.0
500	87.67	99.40	99.99	100.0
750	87.56	99.15	100.0	100.0
1000	86.79	99.01	99.98	100.0
2500	90.06	98.17	99.85	99.94
5000	88.15	95.86	99.48	99.74

Table 4. Table 4: GNN accuracy (%) over test set by threshold versus formula clause widths ( w 𝑤 w ).

$w$	Thresholds
	0.02	0.05	0.10	0.15
3	80.42	98.66	99.87	99.93
5	68.04	96.56	99.90	99.98
8	79.10	97.77	99.96	99.98
13	99.70	99.98	100.0	100.0
21	100.0	100.0	100.0	100.0
34	100.0	100.0	100.0	100.0

Table 5. Table 5: Accuracy (%) by threshold with respect to additive thresholds on size generalization test formulas.

$n$	Thresholds
	0.02	0.05	0.10	0.15
10K	79.89	89.94	97.13	99.71
15K	72.41	81.90	94.83	97.41

Table 6. Table 6: Accuracy (%) by threshold over size generalization test formulas versus w 𝑤 w .

$w$	Thresholds
	0.02	0.05	0.10	0.15
3	78.13	90.63	98.44	100.0
5	73.75	90.0	100.0	100.0
8	76.25	91.25	98.75	100.0
13	40.0	56.25	82.5	95.0
21,34	100.0	100.0	100.0	100.0

Table 7. Table 7: Runtimes (s) for KLM and our GNN by number of variables ( n 𝑛 n ), with w = 3 , 34 𝑤 3 34 w=3,34 and m 𝑚 m = 0.75 n 𝑛 n .

$w$	Algorithm	$n$
		1K	5K	10K	15K
3	KLM	22.59	270.77	1151.86	2375.56
	GNN	0.017	0.040	0.073	0.104
34	KLM	7.62	43.57	164.46	305.61
	GNN	0.020	0.074	0.145	0.223

Table 8. Table 8: Accuracy (%) on all thresholds on training and structure evaluation datasets for ablation study ( T = 2 𝑇 2 T=2 ).

Evaluation Data	Thresholds
	0.02	0.05	0.10	0.15
Training Set	71.84	82.91	91.62	95.18
Test Set	72.08	82.80	91.36	94.97

Table 9. Table 9: Accuracy (%) on all thresholds on size generalization datasets for ablation study ( T = 2 𝑇 2 T=2 ).

$n$	Thresholds
	0.02	0.05	0.10	0.15
10K	71.84	76.72	84.20	89.94
15K	66.37	69.83	79.31	87.93

Table 10. Table 10: Accuracy (%) on all thresholds on training and structure evaluation datasets for T = 32 𝑇 32 {T=32} .

Evaluation Data	Thresholds
	0.02	0.05	0.10	0.15
Training Set	87.68	98.22	99.87	99.99
Test Set	87.32	98.02	99.83	99.95

Table 11. Table 11: Accuracy (%) on all thresholds on size generalization datasets for T = 32 𝑇 32 {T=32} .

$n$	Thresholds
	0.02	0.05	0.10	0.15
10K	74.43	83.91	93.67	96.26
15K	68.97	80.17	87.93	92.24

Table 12. Table 12: Results over other synthetic datasets.

Dataset	Thresholds
	0.02	0.05	0.10	0.15
Fully Privileged	86.33	98.88	99.96	99.99
Meel et al.	88.26	98.67	99.98	100.0

Table 13. Table 13: Runtimes (s) for KLM, GNN by number of variables ( n 𝑛 n ) and width ( w 𝑤 w ) for m 𝑚 m = 0.75 n 𝑛 n .

$w$	Algorithm	$n$
		1K	5K	10K	15K
$3$	KLM	22.59	270.77	1151.86	2375.56
	GNN	0.017	0.040	0.073	0.104
$5$	KLM	15.32	145.47	608.13	1298.38
	GNN	0.017	0.042	0.077	0.110
$8$	KLM	9.32	81.39	322.56	689.50
	GNN	0.017	0.045	0.083	0.121
$13$	KLM	7.07	40.58	158.09	299.26
	GNN	0.017	0.050	0.094	0.138
$21$	KLM	7.26	41.28	157.85	293.83
	GNN	0.018	0.058	0.113	0.167
$34$	KLM	7.62	43.57	164.46	305.61
	GNN	0.020	0.074	0.145	0.223

Equations

$$v_{x,t+1}=combine\Big{(}v_{x,t},aggregate\big{(}N(x)\big{)}\Big{)},$$

$$\displaystyle\hat{v}_{{x_{c}},t+1}=L_{c_{1}}\Big{(}v_{{x_{c}},t},\sum_{x_{l}\in N(x_{l})}M_{l}(v_{x_{l},t})\Big{)}.$$

$$\displaystyle v_{{x_{d}},t+1}=L_{d}\Big{(}v_{{x_{d}},t},\sum_{x_{c}\in N(x_{d})}M_{c}(\hat{v}_{x_{c},t+1})\Big{)}.$$

$$\displaystyle v_{{x_{c}},t+1}=L_{c_{2}}\Big{(}\hat{v}_{{x_{c}},t+1},M_{d}(v_{x_{d},t+1})\Big{)}.$$

$$v_{x_l,t+1}$$

$$\log \hat{\mu }-\log (1+ϵ)\le \log \mu \le \log \hat{\mu }+\log (1+ϵ).$$

$$ELU+1(x)=\{\begin{array}{ll}{e}^{-x}& \text{if}x\le 0\\ x+1& \text{otherwise,}\end{array}$$

$$KL({\mathcal{N}}_1,{\mathcal{N}}_2)=\log \frac{{\sigma }_2}{{\sigma }_1}-\frac{1}{2}+\frac{{\sigma }_1^2+({\mu }_1-{\mu }_2{)}^2}{2{\sigma }_2^2}.$$

$$1+\frac{r\cdot e}{q\cdot n}+\frac{(1-r)\cdot e}{n}=1+\frac{e(q(1-r)+r)}{q\cdot n}.$$

Full text

1 Introduction

Propositional model counting (MC), or #SAT, is the task of counting the number of satisfying assignments for a given propositional formula (?). Weighted model counting (WMC), or weighted #SAT, additionally incorporates a weight function over the set of all possible assignments. Offering an elegant formalism for encoding various probabilistic inference problems, WMC is a unifying approach for inference in a wide range of probabilistic models. In particular, probabilistic graphical models (?), probabilistic planning (?), probabilistic logic programming (?), probabilistic databases (?), and probabilistic ontologies (?) can greatly benefit from advances in WMC.

Two important special cases of WMC are weighted #CNF and weighted #DNF, which require the input formula to be in conjunctive normal form (CNF) and disjunctive normal form (DNF), respectively. Inference in probabilistic graphical models typically reduces to solving weighted #CNF instances, while query evaluation in probabilistic databases reduces to solving weighted #DNF instances (?). However, both weighted #CNF and weighted #DNF are known to be #P-hard (?), and this computational complexity is a major bottleneck for solving large-scale WMC instances.

To overcome this problem, two main paradigms have been developed. The first paradigm is knowledge compilation (?; ?), which solves computationally difficult problems by compiling them into a new representation (i.e., a target language), where they can be subsequently solved efficiently. Following compilation, exact inference in WMC can be done in linear time (?). However, the compilation process can produce exponentially-sized problem representations (i.e., arithmetic circuits). Furthermore, knowledge compilation is not robust to changes: for every change in the underlying model, the computationally demanding knowledge compilation process needs to be repeated. As a result, approaches based on knowledge compilation struggle to scale to large and varying problem instances.

The second paradigm is approximate solving (?; ?; ?), which provides approximations of the model count as opposed to an exact solution. Loosening the requirement for exactitude renders WMC more tractable, especially for #DNF counting, where approximate solving admits a fully polynomial randomized approximation scheme (FPRAS) due to Karp, Luby, and Madras (?), which we denote KLM. KLM allows for faster estimation of #DNF model counts, while also providing probabilistic guarantees on its approximations, and it is the state of the art for weighted #DNF. Nonetheless, KLM runs in $O(nm)$, where $n$ denotes the number of variables and $m$ the number of clauses of the input DNF formula. Hence, KLM struggles to scale to real-world DNF formulas.

In this work, we propose Neural#DNF, an approach that combines deep learning and approximate model counting and enables fast weighted #DNF approximation. We first generate instances of weighted #DNF and solve them using KLM to produce training data. We then use a graph neural network (GNN) to capture the symbolic structure of DNF formulas and train our system. By construction, Neural#DNF produces approximations in $O(m\bar{w})$, where $\bar{w}$ denotes the average clause width. This reduces to just $O(n+m)$ for bounded width. Our approach does not provide guarantees as with KLM, but instead enables a relative speed-up of multiple orders of magnitude in the average case. This is especially true, since, in practice, $\bar{w}<<n$. Our experiments show that the GNN learns to accurately estimate weighted model counts and generalizes to novel formulas. Indeed, our model computes solutions to unseen weighted #DNF instances with $99\%$ accuracy relative to an additive error threshold of $0.1$ with respect to tight KLM approximations. It also generalizes to larger problem instances involving up to 15K variables remarkably well, despite only seeing formulas with at most 5K variables during training.

In summary, Neural#DNF makes the following contributions:

• •

It produces efficient and highly accurate weighted #DNF approximations in $O(m\bar{w})$, and in linear time with bounded width.

• •

It reliably scales to #DNF instances with up to 15K variables, which, to our knowledge, is a first for neural-symbolic methods.

• •

It is robust in that it can produce approximations for any problem instance over a given domain following training.

Our findings suggest that GNNs can effectively and efficiently perform large-scale #DNF through training with dense and reliable data. Further experiments and details are deferred to the appendix of this paper.111The extended version of this paper including the appendix is available at: arxiv.org/pdf/1904.02688.pdf.

2 Preliminaries

We briefly introduce weighted model counting, the KLM algorithm, and graph neural networks.

Weighted Model Counting

Given a (finite) set $S$ of propositional variables, a literal is of the form $v$, or $\neg v$, where $v\in S$. A conjunctive clause is a conjunction of literals, and a disjunctive clause is a disjunction of literals. A clause has width $k$ if it has exactly $k$ literals. A formula $\phi$ is in conjunctive normal form (CNF) if it is a conjunction of disjunctive clauses, and it is in disjunctive normal form (DNF) if it is a disjunction of conjunctive clauses. We say that a DNF (resp., CNF) has width $k$ if it contains clauses of width at most $k$. An assignment $\nu:S\mapsto\{0,1\}$ maps every variable to either [math] (false), or $1$ (true). An assignment $\nu$ satisfies a propositional formula $\phi$, denoted $\nu\models\phi$, in the usual sense, where $\models$ is the propositional entailment relation.

Given a propositional formula $\phi$, its model count $\#\phi$ is the number of assignments $\nu$ satisfying $\phi$. The weighted model count of $\phi$ is given by ${\sum_{\nu\models\phi}w(\nu)}$, where $w:\mathfrak{A}\mapsto\mathbb{R}$ is a weight function, and $\mathfrak{A}$ is the set of all possible assignments. In this work, we set $w:\mathfrak{A}\mapsto[0,1]\cap\mathbb{Q}$ such that every assignment is mapped to a rational probability and ${\sum_{\nu\in\mathfrak{A}}w(\nu)=1}$. As common in the literature, we view every propositional variable as an independent Bernoulli random variable and assign probabilities to literals.

The KLM Algorithm

Exactly solving weighted #DNF instances is #P-hard and thus intractable. The KLM algorithm (?) is a fully polynomial randomized approximation scheme (FPRAS), and provides probabilistic guarantees for weighted #DNF. More formally, given an error $\epsilon>0$ and a confidence value ${0<\delta<1}$, KLM computes $\hat{\mu}$, an approximation of the true weighted model count $\mu$, in polynomial time such that {\Pr\big{(}\mu(1-\epsilon)\leq\hat{\mu}\leq\mu(1+\epsilon)\big{)}\geq 1-\delta}.

Specifically, for a DNF $\phi$ with $n$ variables and $m$ clauses, KLM computes a number of sampling trials ${\tau=8(1+\epsilon)m\log({\frac{2}{\delta}})\frac{1}{\epsilon^{2}}}$, and initializes a trial counter $N$ to [math]. Then, at every trial, KLM performs the following steps:

If no current sample assignment exists, randomly select a clause $C_{i}$ with probability $\frac{p(C_{i})}{\sum_{j=1}^{m}p(C_{j})}$, then randomly generate a satisfying assignment for $C_{i}$ using the variable probability distribution. 2. 2.

Check whether the current assignment satisfies a randomly selected clause $C_{k}$. If so, increment $N$ and generate a new sample assignment. Otherwise, do nothing.

KLM returns $\frac{\tau\sum_{j=1}^{m}p(C_{j})}{mN}$ as an estimate for the weighted DNF count. Since assignment checking runs in $O(n)$, the complexity of KLM amounts to O\big{(}nm\epsilon^{-2}\log(\frac{1}{\delta})\big{)}. KLM is the state of the art for approximate weighted #DNF, so we use it to label DNF formulas used to train our model.

Graph Neural Networks

Graph neural networks (GNNs) (?; ?) are neural networks specifically designed to process structured graph data. In a GNN, every graph node $x$ is given a vector representation $v_{x}$, which is updated iteratively. A node $x$ receives information from its neighborhood $N(x)$, which is the set of nodes connected by an edge to $x$. Let $v_{x,t}$ denote the value of $v_{x}$ at iteration $t$. We write a node update as:

[TABLE]

where combine and aggregate are functions, and aggregate is permutation-invariant. We use layer-norm LSTMs (?) as our combine function, and sum as our aggregate function. This is similar to gated graph neural networks (?), except that we replace the gated recurrent unit (GRU) (?) with a layer-norm LSTM, given the remarkable empirical success of the latter (?; ?). Upon termination of all iterations, the final node representations are used to compute the target output.

GNNs are highly expressive computational models: GNNs can be as discerning between graphs as the Weisfeiler-Lehman (WL) graph isomorphism heuristic (?; ?). Unlike feature engineering (?) and static embedding methods (?), GNNs can autonomously learn relationships between nodes, identify important features, and build models that can generalize to unseen graphs.

3 Graph Neural Network Model

We propose Neural#DNF, a new method for solving weighted #DNF problems based on GNNs. We model DNF formulas as graphs, and use a GNN to iterate over these graphs to compute an approximate weighted model count.

Model Setup

We encode a DNF formula as a graph with 3 layers as shown in Figure 2: a literal layer, a conjunction layer, and a disjunction layer. In the literal layer, every DNF variable is represented by 2 nodes corresponding to its positive and negative literals, which are connected by a (dashed) edge to highlight that they are complementary. In the conjunction layer, every node represents a conjunction and is connected to literal nodes whose literals appear in the conjunction. Finally, the disjunction layer contains a single disjunction node, which is connected to all nodes in the conjunction layer.

To approximate the model count of a DNF formula, we use a message-passing GNN model that iterates over the corresponding DNF graph and returns a Gaussian distribution. Initially, the network computes vector representations for all literal nodes, given their probabilities, using a multi-layer perceptron (MLP) $f_{enc}$. More formally, a $k-$dimensional representation $v_{{x_{i}},0}$ of a literal $x_{i}$ with probability $p_{i}$ is computed as $v_{{x_{i}},0}=f_{enc}(p_{i})$. Nodes in the conjunction and disjunction layers are initialized to two representation vectors $v_{c}$ and $v_{d}$, respectively, and the values for these vectors are learned over the course of training. After initialization, node representations are updated across $T$ message passing iterations.

Message Passing Protocol

A message passing iteration consists of the following 4 steps:

(a) Literal layer nodes compute messages using an MLP $M_{l}$ and pass them to their neighboring conjunction layer nodes. These conjunction nodes then aggregate these messages using the sum function and update their representation using a layer-norm LSTM $L_{c_{1}}$. The updated conjunction node representations, denoted $\hat{v}_{x_{c},t+1}$, are given formally as:

[TABLE]

(b) Conjunction layer nodes compute and send messages to the disjunction node via an MLP $M_{c}$. The disjunction node aggregates these and updates using a layer-norm LSTM $L_{d}$, i.e.,

[TABLE]

(c) The disjunction node computes a message using an MLP $M_{d}$ and sends it to the conjunction nodes, which update their representation using a different LSTM cell $L_{c_{2}}$:

[TABLE]

(d) Using their latest representations, conjunction nodes send messages to neighboring nodes in the literal layer. Literal layer nodes aggregate these messages and concatenate them (represented with $||$) with messages from their corresponding negated literal. Then, they use this message to update their representations using a layer-norm LSTM $L_{l}$:

[TABLE]

A visual representation of the 4 message passing steps for a simple formula is provided in Figure 1. In this protocol, we use 2 distinct LSTM cells $L_{c_{1}}$ and $L_{c_{2}}$ to update the representations of conjunction nodes at steps (a) and (c), so that the network learns separate update procedures for literal-based and disjunction-based updates. At the end of message passing, the final disjunction node representation $v_{x_{d},T}$ is passed through an MLP $f_{out}$. The final layer of this MLP consists of two neurons $n_{\mu}$ and $n_{\sigma}$, which return the mean and standard deviation, respectively, of a predicted Gaussian distribution.

Loss Function

Given $\epsilon$ and $\delta$, KLM returns an estimate $\hat{\mu}$ of the true model count $\mu$ within a multiplicative bound with respect to $\epsilon$, and this bound holds with probability $1-\delta$. By identifying different configurations of $\epsilon$ and $\delta$ that lead to an identical KLM running time, one can deduce that the probability mass is concentrated around $\hat{\mu}$ and decays away from it, and this holds for all DNFs. Note that the multiplicity of the bound interval on $\hat{\mu}$ w.r.t. $\epsilon$ makes it hard to fit standard distributions on it. Hence, we apply a natural logarithm to this bound to get the additive bound on $\log{\mu}$:

[TABLE]

We can then fit a Gaussian $\mathcal{N}(\mu^{\prime},\sigma)$ to this bound by setting $\mu^{\prime}=\hat{\mu}\ \text{and}\ \sigma=\nicefrac{{\log{(1+\epsilon)}}}{{F^{-1}(1-\frac{\delta}{2})}}$, where $F^{-1}$ denotes the inverse cumulative distribution function of the standard Gaussian distribution. The GNN is thus trained to predict $\log{\mu}$, a negative number. We adapt the exponential linear unit (ELU) (?) activation function and apply it to $n_{\mu}$ and $n_{\sigma}$. More specifically, we use

[TABLE]

such that $n_{\mu}$ uses $-ELU+1(x)$, and $n_{\sigma}$ uses $ELU+1(x)$, thereby restricting their outputs to be negative and positive, respectively.

To compare the predicted Gaussian and the KLM result, we use Kullback-Leibler (KL) divergence, which for two Gaussians $\mathcal{N}_{1}(\mu_{1},\sigma_{1})$ and $\mathcal{N}_{2}(\mu_{2},\sigma_{2})$ is given by:

[TABLE]

We set $\mathcal{N}_{1}$ to be the prediction returned by the network and $\mathcal{N}_{2}$ to be the KLM approximation. This choice is critical in order to avoid the system minimizing the training loss by learning to produce arbitrarily large values of $\sigma_{2}$.

4 Experiments

We train our model on a large set of DNF formulas and measure its generalization relative to new DNF formulas. These formulas are distinct in terms of structure (i.e., the underlying clauses and variables in every clause) and size (i.e., the number of clauses and variables is larger), so our experiments target generalization in both aspects. To evaluate structure generalization, we run our GNN on unseen formulas of comparable size to training formulas and measure its performance. To evaluate size generalization, we run tests on novel, larger formulas and assess how well the GNN performs. To further validate our model and data generation procedure, we also run these experiments using differently generated synthetic datasets (?).

Experimental Setup

In our experiments, we compare Neural#DNF predictions $\hat{\mu}$ with those of KLM and check whether their absolute difference falls within pre-defined additive thresholds. We opt for additive error, as opposed to multiplicative error, as the former produces an absolute distance metric, whereas the latter is relative to the model count.

Owing to the lack of standardized benchmarks, we generate synthetic formulas using a novel randomized procedure designed to produce more variable formulas. We generate 100K distinct training formulas, where formula counts per $n$ are shown in Table 1. For every $n$, formulas are generated with fixed clause width $w\in\{3,5,8,13,21,34\}$ and number of clauses $m$ from $\{0.25,0.375,0.5,0.625,0.75\}\cdot n$, such that every valid setting (i.e., all configurations except $w=3$ and $m=0.25\cdot n$) is represented equally, and each formula has 4 variable probability distributions. More details about our data generation can be found in the appendix.

The structure evaluation test set is generated analogously, and contains 13080 distinct formulas. The size evaluation set contains 348 formulas with $n=10K$ and 116 formulas with $n=15K$, with one probability distribution each.

For all experiments, we use $k=128$-dimensional vector representations. We define $f_{enc}$ as a 3-layer MLP with layer sizes 8, 32, and 128, message-generating MLPs ($M_{l}$, $M_{c}$, and $M_{d}$) as 4-layer MLPs with 128-sized layers, and $f_{out}$ as a 3-layer MLP with layers of size 32, 8, and 2. We use the rectified linear unit (ReLU) as the activation function at MLP hidden layers, and linear activation at the output layer for all MLPs except $f_{out}$. For $f_{out}$, output activation is as defined in Section 3. Generated formulas were labelled using KLM with $\epsilon=0.1$ and $\delta=0.05$ to achieve a reasonable trade-off between label accuracy and generation tractability.

We train the system for 4 epochs on a P100 GPU using KL divergence loss, the Adam optimizer (?), a learning rate of $\lambda=10^{-5}$, a gradient clipping ratio of 0.5, and ${T=8}$ message passing iterations.

Results

On the structure generalization test, Neural#DNF predictions align very closely with those of KLM, as shown in Figure 3. The model is within $0.02$ of the KLM WMC estimate over $87.37\%$ of the test set, and this rises to 99.95% for a threshold of $0.1$. The model also performs consistently across different $n$, with accuracy varying by at most $4.5\%$ between any two different $n$ values for all four test thresholds. Overall test results are given in Table 2.

The proximity between training and testing accuracies at all thresholds shows that the network has not fit or memorized its training formulas, but has instead learned a general WMC procedure. The results parametrized by $n$ are provided in Table 3. These results show that the network maintains a high accuracy (e.g., $95.5\%$ for threshold 0.05) across all $n$ values, and so does not rely on a particular $n$ to achieve its high overall performance. Notably, the model is also robust against variation in $w$. As shown in Table 4, the model scores above $96\%$ and $99\%$ across all widths for thresholds $0.05$ and $0.1$, respectively. Interestingly, it has near-perfect performance for larger widths 13, 21, and 34, where weighted model counts are near-zero, and has relatively higher accuracy at threshold $0.02$ when $w=3$, where counts are almost one. Simultaneously performing well in both extreme cases, coupled with high accuracy on intermediate widths, further highlights the robustness of our model.

On the size generalization task, our model maintains accuracies of $97.13\%$ and $94.83\%$ with a threshold of $0.1$ on 10K and 15K-variable formulas, respectively, despite having as many as triple the variables as in training. The full results for size generalization are given in Table 5. The same results parametrized by width $w$ are also given in Table 6. These show that the network performs consistently across widths 3, 5, and 8, but performs less well at $w=13$. This is due to formulas with $w=13$ exhibiting a “phase transition” at this $n$ and $m$. Indeed, in this setting, model counts fluctuate dramatically, since $m$ is in the same order of magnitude as $p^{-1}$, the inverse expected clause satisfaction probability. In the training set, this phenomenon occurs at smaller widths, but never for $w=13$, so this is an entirely new situation for the model, at a much larger scale. Nonetheless, it achieves an encouraging accuracy of $82.5\%$ for the threshold $0.1$.

These results show that reliable approximate model counting on large-scale formulas can be achieved, even with training restricted to smaller formulas. From a practical perspective, this gives further evidence that large-scale solvers can be trained using smaller formulas that are tractably labelled with existing solvers. In additional experiments run on differently generated datasets (cf. appendix), our system also maintains very high performance, and in fact performs better on fully random formulas (?) than on formulas generated with our protocol. This further highlights the robustness of Neural#DNF, and validates the quality of our data generation procedure.

For all these results, message passing iterations are essential. Indeed, when run with just 2 message passing iterations for our ablation study, the GNN performs significantly worse across all experiments. However, this does not imply that performance always improves with more message passing. In fact, running too many message passing iterations makes the system prone to overfitting: When run with 32 iterations, the system achieves a similar performance in structure generalization, but its performance drops significantly in size generalization. This shows that a trade-off value of message passing iterations, in our case 8, must be selected, to enable sufficient communication, while not encouraging overfitting. Further details on our ablation study and experiments with 32 iterations can be found in the appendix.

All in all, our model achieves remarkable performance both in terms of structure and size generalization. These results highlight the power and scalability of neural message passing (NMP) methods to perform advanced reasoning tasks, and therefore justify further consideration of NMP.

Running Time Analysis

In the average case, our GNN runs in $O(m\bar{w})$, where $\bar{w}$ denotes the average formula clause width. By contrast, KLM runs in $O(nm)$, so is much slower for standard cases in practice, where $\bar{w}<<n$. In the worst case, our GNN runs in $O(nm)$, which is asymptotically identical to KLM. However, in a best-case scenario where $\bar{w}$ is upper-bounded, the GNN complexity drops to just $O(n+m)$, enabling linear-time approximations to be made, whereas KLM remains $O(nm)$, since its complexity does not depend on $\bar{w}$. Hence, our system enables much faster approximations than KLM in practice, where $\bar{w}<<n$, and these approximations are in linear time with bounded clause width $\bar{w}$. A detailed complexity analysis for Neural#DNF can be found in the appendix.

Furthermore, our GNN runs on graphics processing units (GPUs) and thus benefits from accelerated computation. We show running times for the GNN vs. KLM ($\epsilon=0.1$, $\delta=0.05$) for formulas with ($w=3,34$, $m$ = 0.75$n$) at every $n$ in Table 7, and running times for all widths are provided in the appendix. However, we note that KLM and the GNN ran over different hardware (Haswell E5-2640v3 CPU vs. P100 GPU, resp.), since they are best suited to their respective devices (CPUs more efficiently handle multiple operations, like sampling, slicing, and comparison, whereas GPUs are efficient for repetitive floating point operations). Hence, these running times are only provided to highlight the scalability of the GNN with increasing formula size, which supports the formal running time expectations of the respective algorithms. Indeed, KLM requires $7.62$ seconds for $w=34,n=1K$, and this rises rapidly to $305.61$s for $w=34,n=15K$, whereas the GNN only needs $0.02$ and $0.223$ seconds, respectively. This is because the GNN takes advantage of limited width to deliver linear scalability, while KLM scales quadratically with $n$ and $m$.

Finally, the GNN does not perform slower at smaller widths as with KLM, as it does not rely on sampling. With KLM, random assignments are replaced when they satisfy a clause, which means that with smaller clause widths, more replacements are made, as clause satisfaction is more likely, and this causes a heavy computational overhead. For example, KLM needs 2375 seconds (about 40 minutes) to run on a formula with $n=15K$ and $w=3$, using $\epsilon=0.1$ and $\delta=0.05$, whereas it only requires 306s when $w=34$. By contrast, the GNN requires only 0.104 and 0.223 seconds, respectively.

Discussions: Analyzing the Model

To examine how our model makes predictions, we selected 21 formulas $f_{i}:i\in[1,21]$ from the structure test set with weighted KLM model counts of roughly $\frac{21-i}{20}$. We then ran our GNN model on these formulas and computed the predicted probability at the end of every message passing iteration. Results are visualized in Figure 4. Initially, the network starts with a low estimate. Then, in the first 3 iterations, it accumulates probabilities and hits a “spike”, which can be mapped to messages from literal nodes reaching the disjunction node. Following this, the network lowers its estimates, before adjusting and refining them in the final iterations.

Unlike (?), where the estimate of satisfiability increases mostly monotonically, our network estimates fluctuate aggressively. A large initial estimate is made, and then reduced and refined. In doing so, the network seems to be initially estimating the naive sum of conjunction probabilities, and subsequently revisiting its estimates as it better captures intersections between conjunctions. This falls in line with our observations, as any understanding of intersections can only occur starting from the third iteration, when the disjunction and conjunction nodes will have passed each other more global information. This also explains the limited performance observed in our ablation study: With just 2 iterations, the system cannot capture conjunction intersections, so can only make naive estimates.

5 Related Work

Weighted #DNF belongs to the wider family of WMC problems, which have been extensively studied due to their connection with probabilistic inference. Weighted #DNF is #P-hard (?), so is highly intractable. In fact, Toda proved that the class $\textsc{P}^{\textsc{\#P}}$ contains the entire polynomial hierarchy (?). Surprisingly, even weighted #DNF counting on positive, partitioned DNF formulas with clause width at most $2$ (?) remains #P-hard.

As a result, many methods have been developed to exactly solve or approximate WMC solutions. One such method is knowledge compilation (KC), where WMC problems are compiled into a new representation in which they are solved efficiently and exactly. KC pushes computational overhead to a preprocessing phase, but compensates for this by subsequently enabling efficient, linear-time probabilistic inference (?). However, compiled representations can be of exponential size in the worst-case. Hence, KC has limited scalability and robustness to model change, which has motivated research in approximate KC (?; ?). Our model training emulates KC preprocessing, but ultimately our model provides approximations and is more scalable. Moreover, it is robust to input changes, as it conceptually handles any formula over a fixed domain of variables and any probability distribution.

Another important paradigm is to produce approximate solutions to circumvent the intractability of WMC (?). For the unweighted case (MC), hashing-based methods (?; ?) (see also (?)) produce an approximation with probabilistic guarantees. Importantly, (?) also yields an FPRAS when restricted to unweighted DNF; see, e.g., (?). For hashing methods, approximation-preserving reductions from WMC to MC are known for CNF, but this remains open for the case of DNF (?). Hence, none of these hashing methods apply to weighted #DNF. Beyond hashing techniques, loopy belief propagation (LBP) (?; ?) has been applied to approximate WMC. LBP does not provide any guarantees (?). Conceptually, our work also uses message passing, but instead learns messages and states so as to best capture the necessary information to relay. It also restricts all outgoing messages from a node to be identical.

Our work builds on recent applications of GNNs (?) to a variety of reasoning tasks, such as solving SAT (?) and the traveling salesman problem (TSP) (?). There has also been work towards outright learning of inference in probabilistic graphical models (?). These works achieve encouraging results, but only on very small instances (i.e., $\sim$40 variables) of their respective problems. Indeed, they struggle to generalize to larger (but still small) instances. This is expected, since SAT and TSP are NP-complete and are hard to approximate with strong guarantees. Similarly, probabilistic inference in graphical models is #P-hard and remains NP-hard to approximate (as is weighted #CNF). Thus, significant work must be done in this direction to reach results of practical use. In contrast, our work tackles a problem with a known polynomial-time approximation, and learns from a dense dataset of approximate solutions with a very high accuracy at a large scale, and can generalize even further with tolerable loss in performance. To our knowledge, our model is the first proposal that combines reasoning and deep learning, while also scaling to realistic problem instance sizes.

6 Summary and Outlook

We presented Neural#DNF, a neural-symbolic approach that leverages the traditional KLM approximate weighted #DNF counter and GNNs to produce weighted #DNF approximations. This work shows that neural networks can be effectively and efficiently applied to large-scale weighted #DNF, given sufficiently dense and reliable training data. Therefore, it is particularly useful for query evaluation on large online probabilistic databases, where queries have computational limitations (?).

Looking forward, we will analyze the viability of GNNs for other reasoning problems, particularly in light of their expressive power, which could be limiting for problems with less structured graph representations. We hope that this work inspires further research leading to less data-dependent neural-symbolic methods, and a greater understanding of neural method performance over challenging problems.

7 Acknowledgements

This work was supported by the Alan Turing Institute under the UK EPSRC grant EP/N510129/1, the AXA Research Fund, and by the EPSRC grants EP/R013667/1, EP/L012138/1, and EP/M025268/1. Ralph Abboud is funded by the Oxford-DeepMind Graduate Scholarship and the Alun Hughes Graduate Scholarship. Experiments for this work were conducted on servers provided by the Advanced Research Computing (ARC) cluster administered by the University of Oxford.

Appendix A Details of Data Generation

Standard Generation Procedure

To generate data, we develop a comprehensive randomized generation procedure, which takes as input the target number of variables $n$, the target number of clauses $m$, and minimum and maximum bounds $\mathsf{minW}$ and $\mathsf{maxW}$ on clause widths $w$ within the formula. In the paper, we use fixed-width clauses, hence, set $\mathsf{minW}=\mathsf{maxW}=w$. Initially, the procedure randomly generates $m$ clause widths using a uniform distribution bounded between $\mathsf{minW}$ and $\mathsf{maxW}$ inclusive. It then computes their sum, which we call the slot count $s$, and continues generation only if ${s\geq n}$. It then allocates the $s$ slots to the $n$ variables, such that every variable is allocated at least one slot, ensuring all variables appear in the generated formula. This is equivalent to the combinatorial problem of putting $k$ balls into $n$ boxes such that no boxes are empty.

Once all variable allocations are determined, all variables are sorted in decreasing allocation order and then assigned to clauses in that order. This ensures that more prominent variables, which appear more in the formula, are accommodated first, when more empty slots are available, thus maximizing the likelihood of generation success. In this assignment phase, a variable having $s$ slot allocations will be assigned to $s$ clauses by randomly, selecting these clauses from the $m$ total clauses without replacement. This ensures no variable is assigned to the same clause twice, to prevent redundancy. Further heuristics are also added to this mechanism to prioritize selecting clauses with more empty slots at this phase, so that all clauses are filled in a uniform fashion. At the end of variable assignment to clauses, all variable instances are individually randomized to be positive or negative literals.

Probabilities for variables are chosen uniformly at random. In our experiments, we use 4 distributions for every formula in our training and evaluation sets, such that one distribution is randomly generated, and the other 3 distributions are quarter increments of the random distribution modulo 1. For example, if a variable $v_{1}$ is assigned probability $0.1$ for the random distribution, it will have probabilities $0.35$, $0.6$, and $0.85$, respectively, in the 3 other distributions. This ensures that we produce formulas with model counts covering the entire $[0,1]$ range as evenly as possible, so as to have more representative training and testing data.

Adding Non-uniformity to Generation

In the standard generation procedure presented earlier, every variable appears between 1 and $m$ times in a formula, and $\frac{S}{n}$ times in expectation. However, it is highly unlikely, by the Chernoff bound, to produce formulas with high dependence on a small subset of variables, i.e., with some variables appearing far more frequently than others and across a majority of clauses. Thus, with very high probability, formulas generated according to this procedure will have their weighted model count depend almost exclusively on clause widths and $m$, with individual variables having very little impact on the model count. This is highly undesirable, as it prevents the network from learning the contributions of individual variables, and encourages overfitting to higher-level structural details of the formula, namely, $w$ and $m$.

To tackle this, we introduce two new variables ${q,r\in[0,1]}$. These variables create a set of $p=q\cdot n$ privileged variables, which will appear far more frequently than their non-privileged counterparts and impact the model counts more severely. These variables are exclusively assigned $r\cdot e$ slots at random, where $e$ is the excess slots $e=s-n$. The remaining $s-e\cdot r$ slots are then subsequently allocated to all variables (including privileged ones) using the standard generation procedure, and assignment to clauses is done analogously afterwards. Therefore, the expected number of allocations for a privileged variable $v_{priv}$ given non-zero values of $q$ and $r$ is:

[TABLE]

To further enforce dependence on privileged variables, all corresponding privileged literals for a privileged variable are randomised together, such that they all are unanimously positive or negative. This makes that all clauses require the same assignment of the privileged variable, and that no mutually exclusive clauses are created, which would greatly increase formula counts and reduce variability. Therefore, literals of privileged variables are all set to the same sign to give them more impact on the model count

Generating Formulas for Experiments

When generating formulas for the experimental data sets, we set $q=0$ and $r=0$ with probability 0.5, and therefore generate 50% of our formulas without privileged variables. For the remaining 50%, we sample $q$ from an exponential distribution with $\lambda=1$, take the remainder of this value modulo $\frac{\log{(n)}}{n}$, and round this value up to the nearest multiple of $\frac{1}{n}$. This privileged variable selection process is highly selective. In fact, this process becomes increasingly selective as $n$ increases, since $\lim_{n\to\infty}\frac{\log{(n)}}{n}=0$. As a result, privileged variables have a strong effect on the formula model count. With q set, we finally, set $r$ as being the value for which generation can succeed (i.e., no privileged variable gets allocated more than the number of clauses) with probability at least 0.5 by a one-sided Chebyshev bound.

Appendix B Further Experiments

Ablation Testing

To evaluate the role of message passing for model performance, we ran the same experimental protocol as in Section 4 using only $T=2$ iterations for both training and testing. With 2 iterations, only one full pass through the 3 network layers is possible: in the first iteration, literal node messages update all conjunction node states, and in the second iteration, these nodes provide a meaningful update to the disjunction node. With this configuration, we observed a large drop in system performance, both in terms of structure and size generalization. The results of this experiment are provided in Tables 8 and 9. From this, we learn that message passing is essential to model performance. Indeed, the model cannot deliver a reliable estimate within just 2 iterations, as it cannot learn about intersections between clauses, thereby limiting it to naive guesses based on disjoint unions. This is also evidenced in Figure 4, where this phenomenon occurs within the first 2 iterations of the 8-iteration set.

Experiments with More Iterations

In addition to our ablation study, we also train and run our system using ${T=32}$ message passing iterations. With this many iterations, the system is expected to build a more comprehensive understanding of connections between different components of the graph, and so should perform better. However, we found that this was not the case. In terms of structure generalization (Table 10), the system achieves similar performance compared with $T=8$, but performs significantly worse in terms of size generalization (Table 11). This shows that the system overfits with too many iterations, such that it learns a message passing optimized for its training set, but cannot generalize to larger formulas.

Results on Other Datasets

We generated two new synthetic datasets of identical size and composition to the original structure evaluation set. The first dataset is entirely based on our generator, such that privileged variables are always used during generation (in the main experiments, this is only used 50% of the time). As a result, this dataset consists entirely of formulas where a small subset of variables have a major effect on the overall weighted model count. We refer to this dataset as Fully Privileged.

The second dataset, on the other hand, is generated using a random generator similar to the one used in (?), where variables and clauses are generated and allocated uniformly at random, and we call it the Meel et al. dataset. We evaluated our model on both these sets, and show results in Table 12. Our system performs very well on the “privileged” data set, in close proximity to original test set performance, and actually performs better on the fully random dataset. This is not surprising, as (?) allocates variables uniformly, thus producing formulas with model counts that can be statistically approximated more easily. These results highlight the robustness of our GNN, and also show the quality of our generation procedure.

Appendix C Complexity of Algorithms

Let $n$ be the number of variables in a DNF formula, $m$ be the number of clauses, and $\bar{w}$ be the average clause width. We show that our tool has average-case complexity $O(m\bar{w})$ and is therefore more efficient than KLM, which has complexity O\big{(}nm\epsilon^{-2}\log(\frac{1}{\delta})\big{)}, since, in practice, $\bar{w}<<n$:

• •

In a message passing iteration, $2\sum_{i=1}^{m}w_{i}$ messages are passed between literal layer nodes and conjunction layer nodes, where $w_{i}$ denotes the width of clause $i$. $2\sum_{i=1}^{m}w_{i}$ can be rewritten as $2m\bar{w}$, where $\bar{w}=\frac{1}{m}\sum_{i=1}^{m}w_{i}$.

Furthermore, $2n$ messages pass between literal nodes and their negations, and $2m$ messages pass between conjunction nodes and the disjunction node. All messages are summed at their respective destinations, thus yielding as many additions as messages passed. Following this, $2n+m+1$ constant-time state updates are made. Since every variable is assumed to appear in a clause, we always have that $n\leq mw$. As a result, the average-case complexity of a message passing iteration is $O(m\bar{w})$. Finally, since the number of message passing iterations $T$ is fixed, we deduce that the average-case GNN complexity is also $O(m\bar{w})$, which is significantly better than KLM’s O\big{(}nm\epsilon^{-2}\log(\frac{1}{\delta})\big{)}, particularly since ${\bar{w}<<n}$, in practice.

• •

Even in the worst-case where all clauses have width $n$, ${2nm}$ messages are passed between literals nodes and conjunctions nodes, and the GNN therefore has complexity ${O(nm)}$, which is asymptotically identical to KLM.

• •

In the best-case, when clause width is upper-bounded by a constant, the number of messages passed becomes ${O(n+m)}$. And since state updates are also $O{(n+m)}$, the complexity of an iteration therefore reduces to ${O(n+m)}$, allowing for linear-time estimation of weighted DNF counts.

Appendix D Algorithm Running Times

KLM ran on a single Haswell E5-2640v3 CPU, which has a clock speed of 2.60GHz. This CPU was part of a node with has 64 GB of memory. Our GNN ran on a Tesla P100 GPU, which has 12 GB of on-device memory. Running times for both algorithms were measured across 50 runs and averaged to produce the results in Table 13.