Mar, 2023

带量词求解器的通用布尔公式最小化

HTML
PDF
TL;DR该研究旨在解决将命题公式转化为任意格式的等价公式的问题，使用量子布尔公式编码的方法可以有效地解决此类问题，因为这种方法远优于使用暴力方法或者SAT求解器进行转化。
发现论文，激发创造
  • 精确模型计数的下界及在概率数据库中的应用

    本文研究了用于准确计算布尔公式的确定性决策图(d-DNNF)表示法，将其转换为自由二叉决策图(FBDD)用于提供计算上限，并证明了决策-DNNF的指数下限，从而提高了关联概率数据库的计算效率。

    Sep, 2013

  • 伪布尔约束的BDDs新视角

    该研究论文主要研究了基于二元决策图的 Pseudo-Boolean 约束编码技术，提出了使用系数分解方法克服爆炸性增长问题，并给出了第一个多项式广义弧一致的 ROBDD 编码算法。

    Jan, 2014

  • QBF作为Courcelle定理的替代

    本文采用量化布尔公式减少作为一种新的方法来展示固定参数线性算法，研究人工智能领域的几个已知问题，其中大部分问题已经通过使用 Courcelle 定理或动态规划证明了其固定参数线性，但作者认为采用 量化布尔公式 减少这种方法具有明显的优势。

    May, 2018

  • 基于树宽求解问题的高级工具和方法 - 扩展摘要

    本文主要研究了基于逻辑的问题及基于treewidth的方法和工具，并提出了一种新类型的问题降解方法，其中问题为有界treewidth的量化布尔公式（QBF）。结果表明，treewidth是设计现代求解器时应考虑的一项重要的测量标准。

    Aug, 2022

  • 显式依赖合成

    该研究提出一种名为Manthan3的数据驱动的方法，用于解决依赖量化布尔公式中的Henkin合成问题，实现对线路的验证、控制器合成和线路实现等应用方面具有积极的意义。

    Jan, 2023

  • 一阶逻辑双变量片段中的精确采样

    本文研究了最近由Wang等人提出的一阶逻辑采样问题——如何在有限域上高效地采样给定一阶句子的模型？我们将他们对于双变量逻辑FO^2的普遍量化子片段UFO^2的结果扩展到整个FO^2片段。具体来说，我们证明了FO^2在采样下的域可扩展性，即存在一种能在域大小多项式时间下运行的FO^2采样算法。然后，我们进一步表明，即使存在像所有x存在= ky: φ（x，y）和存在= kx为所有y的数量约束，如φ（x，y）的量化器公式，我们的方法也可以保持运作。我们的提出的方法是具有建设性的，由此产生的采样算法在各个领域都有潜在的应用，包括在组合结构和统计关系模型的均匀生成方面以及如Markov逻辑网络和概率逻辑程序的采样方面。

    Feb, 2023

  • ASP(Q)的高效求解器

    本文介绍了一种新的 Answer Set Programming with Quantifiers ASP(Q) 的实现方式，它构建在 qasp 的基础上，具有更高效的编码过程和自动选择多个 QBF-solving 后端的算法选择策略，具有比 qasp 更好的性能表现。

    May, 2023

  • 构建精确的伪布尔模型计数器

    我们提出了第一个准确的伪布尔模型计数器PBCount，它通过代数决策图的知识编译方法来实现。我们的实证评估表明，PBCount可以计算1513个实例的计数，而当前最先进的方法只能处理1013个实例。我们的工作为进一步研究伪布尔公式的模型计数提供了几个方向，如预处理技术的开发和除知识编译之外的其他方法的探索。

    Dec, 2023

  • 求解具有少量存在变量的量化布尔公式

    通过对存在量化变量数量的参数化，我们开发了一种适用于有界子句长度的共价正常形式（CNF）QBF实例的新型固定参数可解性算法。

    May, 2024

  • 一种基于存在图的系统命题公式简化框架

    本文介绍了一种基于Peirce的存在图推理和蕴含图的命题逻辑简化演算法，该算法可以应用于嵌套形式的命题逻辑公式，保持等价性、保证变量、子句和文字数量的单调递减，并最大限度地保留结构问题信息；同时，提出了一个系统化应用两个规则（EPR和TWSR）的简化过程，可用于简化大型布尔可满足性问题和任意形式的命题公式，并对其在空间和时间方面进行了算法复杂性的形式分析；最后，展示了如何通过引入一种新的n元蕴含图扩展我们的规则，以涵盖所有已知的等价性保持预处理过程。

    May, 2024