Nov, 2014

SMT 中的近似计数和概率程序的值估计

PDF
TL;DR本篇论文介绍了一种从 SMT 到 #SMT 近似版本的约简方法，并提出了关于整数算术和线性实数算术的模型计数算法，通过对现代 SMT 求解器的高级启发式算法进行利用，运行时间为多项式级别并提供正式边界。我们使用这些算法来解决带有非确定性的无循环概率程序模型的值问题。
smtmodel countinginteger arithmeticlinear real arithmeticprobabilistic programs
发现论文，激发创造
  • 可扩展的近似模型计数器

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

    Jun, 2013

  • 稳定模型计数及其在概率逻辑编程中的应用

    本文研究了使用稳定模型语义进行推理的问题，提出了两种基于未建立的集合检测的实现技术，扩展了命题模型计数器到稳定模型计数器，可以在时间和空间使用方面显著优于现有的解决方案。

    Nov, 2014

  • 四舍五入 meets 近似模型计数

    研究了哈希算法在计算 Boolean 公式中的模型数量时，delta 值较小会对可伸缩性造成重大影响。提出了一种基于 Rounding 的新方法和一种新算法（RoundMC），用于高置信度下的估计，可以显著提高运行时性能。RoundMC 能够比当前技术水平更好地解决问题，速度提高了 4 倍。

    May, 2023

  • 正式验证的近似模型计数

    我们提出了第一个近似模型计数的认证框架，并且证明了其输出近似值的质量保证。

    Jun, 2024

  • 线性有理代价理论模优化

    本文介绍了两种使用 SMT 解决带有线性有理成本函数最小化的一般性过程，并将其与标准最小化技术相结合。我们已将程序封装在 MathSAT SMT 求解器内，并成功与其他最先进的工具在 Linear Generalized Disjunctive Programming 领域中进行了实验。结果表明，我们的工具在这些问题上是非常有竞争力的，并且在许多情况下表现更好，展示了该方法的潜力。

    Oct, 2014

  • 基于 SMT 的递归程序模型检查

    这篇论文介绍了一种基于 SMT 的符号模型检查算法，适用于递归程序的安全验证，通过维护 “上 / 下估计” 来分析单个过程，有助于检测出最终证明及阻止非可行的反例，该算法还实现了量词消除，使得在可判定理论下，算法可以确保找到反例。

    May, 2014

  • 用于近似模型计数的可审计算法

    模型计数、近似计数算法、可审核的近似计数器、证书和 oracle

    Dec, 2023

  • 通过字级计数进行概率近似推断

    该研究提出了一种基于单词级哈希函数的模型计数方法，可以直接利用复杂的 SMT 求解器，为概率推理中的计数问题提供了新思路。

    Nov, 2015

  • 投影模型计数

    本文介绍了优先变量，非优先变量，以及计算仅涉及优先变量的模型计数问题，探讨了三种不同的计数方法，并在多组实验结果上进行了比较。

    Jul, 2015

  • 解决符号与统计人工智能集成的可证明保证下的可满足性模数计数

    通过使用 XOR-SMC，我们提出了一种多项式算法，用于解决高度棘手的 SMC 问题，该算法具有恒定近似保证，并通过将 SMC 中的模型计数替换为受随机 XOR 约束的 SAT 公式，将高度棘手的 SMC 转化为可满足性问题。我们在 AI 有益于社会的重要 SMC 问题的求解实验中展示了 XOR-SMC，它找到了接近真实最优解的解决方案，胜过了几个难以找到可靠逼近 SMC 中棘手模型计数的基线方法。

    Sep, 2023