近似模型计数，Sparse XOR约束和最小距离

作者：Michele Boreale,Daniele Gorla

摘要：计算给定布尔公式的模型数量的问题具有许多应用，包括计算定量信息流中的确定性程序的泄漏。模型计数是一个很难的#P完全问题。出于这个原因，在过去十年中已经开发了许多近似计数器，提供了信心和准确性的正式保证。一种流行的方法是基于使用随机XOR约束的概念，粗略地，连续地将解决方案集减半，直到没有模型为止：这通过调用SAT求解器来检查。这个过程的有效性取决于SAT求解器处理XOR约束的能力，而XOR约束反过来又取决于这些约束的长度。我们研究在多大程度上可以采用稀疏的，因此短的约束，保证正确性。我们证明了结果边界与模型集的几何形状密切相关，特别是模型之间的最小汉明距离。我们在一些具体公式上评估我们的理论结果。根据我们的研究结果，我们最终讨论了在近似模型计数中改进现有技术水平的可能方向。

原文标题：Approximate Model Counting, Sparse XOR Constraints and Minimum Distance

原文摘要：The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is based on the idea of using random XOR constraints to, roughly, successively halving the solution set until no model is left: this is checked by invocations to a SAT solver. The effectiveness of this procedure hinges on the ability of the SAT solver to deal with XOR constraints, which in turn crucially depends on the length of such constraints. We study to what extent one can employ sparse, hence short, constraints, keeping guarantees of correctness. We show that the resulting bounds are closely related to the geometry of the set of models, in particular to the minimum Hamming distance between models. We evaluate our theoretical results on a few concrete formulae. Based on our findings, we finally discuss possible directions for improvements of the current state of the art in approximate model counting.

地址：https://arxiv.org/abs/1907.05121