Propositional model counting (#SAT) can be solved efficiently when the input
formula is in deterministic decomposable negation normal form (d-DNNF).
Translating an arbitrary formula into a representation that allows inference
tasks, such as counting, to be performed efficiently, is called knowledge
compilation. Top-down knowledge compilation is a state-of-the-art technique for
solving #SAT problems that leverages the traces of exhaustive DPLL search to
obtain d-DNNF representations. While knowledge compilation is well studied for
propositional approaches, knowledge compilation for the (quantifier free)
counting modulo theory setting (#SMT) has been studied to a much lesser degree.
In this paper, we discuss compilation strategies for #SMT. We specifically
advocate for a top-down compiler based on the traces of exhaustive DPLL(T)
search.

该研究讨论了 #SMT 的编译策略，提出了一种基于穷尽 DPLL (T) 搜索的自上而下的编译器。

自顶向下计数模理论知识编译

Top-Down Knowledge Compilation for Counting Modulo Theories

Graph Neural Networks (GNNs) have been recently leveraged to solve several
logical reasoning tasks. Nevertheless, counting problems such as propositional
model counting (#SAT) are still mostly approached with traditional solvers.
Here we tackle this gap by presenting an architecture based on the GNN
framework for belief propagation (BP) of Kuch et al., extended with
self-attentive GNN and trained to approximately solve the #SAT problem. We ran
a thorough experimental investigation, showing that our model, trained on a
small set of random Boolean formulae, is able to scale effectively to much
larger problem sizes, with comparable or better performances of state of the
art approximate solvers. Moreover, we show that it can be efficiently
fine-tuned to provide good generalization results on different formulae
distributions, such as those coming from SAT-encoded combinatorial problems.

本研究将自我注意的图神经网络应用于基于 BP 的计数问题，成功地在产生概率接近于技术先进的问题解决器的解的同时，保证了模型性能的扩展性。

命题模型计数的图神经网络

Graph Neural Networks for Propositional Model Counting

Propositional model counting is a fundamental problem in artificial
intelligence with a wide variety of applications, such as probabilistic
inference, decision making under uncertainty, and probabilistic databases.
Consequently, the problem is of theoretical as well as practical interest. When
the constraints are expressed as DNF formulas, Monte Carlo-based techniques
have been shown to provide a fully polynomial randomized approximation scheme
(FPRAS). For CNF constraints, hashing-based approximation techniques have been
demonstrated to be highly successful. Furthermore, it was shown that
hashing-based techniques also yield an FPRAS for DNF counting without usage of
Monte Carlo sampling. Our analysis, however, shows that the proposed
hashing-based approach to DNF counting provides poor time complexity compared
to the Monte Carlo-based DNF counting techniques. Given the success of
hashing-based techniques for CNF constraints, it is natural to ask: Can
hashing-based techniques provide an efficient FPRAS for DNF counting? In this
paper, we provide a positive answer to this question. To this end, we introduce
two novel algorithmic techniques: \emph{Symbolic Hashing} and \emph{Stochastic
Cell Counting}, along with a new hash family of \emph{Row-Echelon hash
functions}. These innovations allow us to design a hashing-based FPRAS for DNF
counting of similar complexity (up to polylog factors) as that of prior works.
Furthermore, we expect these techniques to have potential applications beyond
DNF counting.

本文研究了命题模型计数问题，针对约束条件表达式分别为 DNF 公式和 CNF 公式分别介绍了 Monte Carlo 和基于哈希的计数技术，并提出了两种新算法技术：Symbolic Hashing 和 Stochastic Cell Counting，通过设计基于哈希的 FPRAS for DNF counting 提高了效率和应用价值。

基于哈希的近似 DNF 计数方法

On Hashing-Based Approaches to Approximate DNF-Counting

Propositional model counting} (#SAT), i.e., counting the number of satisfying
assignments of a propositional formula, is a problem of significant theoretical
and practical interest. Due to the inherent complexity of the problem,
approximate model counting, which counts the number of satisfying assignments
to within given tolerance and confidence level, was proposed as a practical
alternative to exact model counting. Yet, approximate model counting has been
studied essentially only theoretically. The only reported implementation of
approximate model counting, due to Karp and Luby, worked only for DNF formulas.
A few existing tools for CNF formulas are bounding model counters; they can
handle realistic problem sizes, but fall short of providing counts within given
tolerance and confidence, and, thus, are not approximate model counters.
We present here a novel algorithm, as well as a reference implementation,
that is the first scalable approximate model counter for CNF formulas. The
algorithm works by issuing a polynomial number of calls to a SAT solver. Our
tool, ApproxMC, scales to formulas with tens of thousands of variables. Careful
experimental comparisons show that ApproxMC reports, with high confidence,
bounds that are close to the exact count, and also succeeds in reporting bounds
with small tolerance and high confidence in cases that are too large for
computing exact model counts.

介绍了一种基于 SAT 求解器的算法和实现工具，用于处理大规模的 CNF 公式的近似计数问题。通过多项式调用的方式，能够高精度地估算满足条件的解数，同时针对过大的问题仍能提供高置信度的估算边界。