专栏首页算法和应用近似模型计数,Sparse XOR约束和最小距离
原创

近似模型计数,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

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 计算的度量集中度:最佳界限,减少量等

    作者:Omid Etesami,Saeed Mahloujifar,Mohammad Mahmoody

    罗大琦
  • 体积正则图的逐步社区检测

    作者:Luca Becchetti,Emilio Cruciani,Francesco Pasquale,Sara Rizzo

    罗大琦
  • 从Splay到动态优化的新路径

    摘要:考虑在二叉搜索树中执行搜索序列的任务。 在每次搜索之后,允许算法以与执行的重构量成比例的成本任意地重构树。 执行的成本是搜索所花费的时间和使用重组操作优化...

    罗大琦
  • ASP.NET MVC 5 Authentication Breakdown

    In my previous post, "ASP.NET MVC 5 Authentication Breakdown", I broke down all ...

    阿新
  • Codeforce 1102 C. Doors Breaking and Repairing

    You are policeman and you are playing a game with Slavik. The game is turn-based...

    风骨散人Chiam
  • 研发:What is a DDoS Attack?

    A distributed denial-of-service (DDoS) attack is a malicious attempt to disrupt ...

    heidsoft
  • 步进式的框架解释如何解决约束满足问题(CS AI)

    我们以逻辑网格难题的用例探讨逐步解释如何解决约束满足问题的问题。更具体地说,我们研究一种以易于理解的方式解释传播过程中可以采取的推理步骤的问题。因此,我们旨在为...

    刘子蔚
  • 数据定制索引的代价:病毒对学习型索引结构的攻击 (CS CR)

    学习型索引结构的概念依赖于这样一种想法,即数据库索引的输入输出功能可以被看作是一种预测任务,因此,可以使用机器学习模型而不是传统的算法技术来实现。这个新颖的角度...

    Antonia
  • Instant Messaging at LinkedIn: Scaling to 10000 of Connections

    We recently introduced Instant Messaging on LinkedIn, complete with typing indic...

    首席架构师智库
  • 【Codeforces】1213A - Chips Moving

    版权声明:本文为博主原创文章,遵循 CC 4.0 BY-SA 版权协议,转载请附上原文出处链接和本声明。 ...

    喜欢ctrl的cxk

扫码关注云+社区

领取腾讯云代金券