Dec, 2022

BNSynth: 有界布尔函数综合

PDF
TL;DR该论文介绍了一种名为 BNSynth 的工具，它是解决具有解决方案空间范围限制的 BFS 问题的第一个工具，该工具利用反例指导的神经方法去综合较小的函数，并且相比现有的工具，平均方案大小减少了至少 3.2 倍（最高可达 24 倍）。
发现论文，激发创造
  • BoSy: 一个有界综合实验框架

    介绍了基于有界综合方法的反应式综合工具 BoSy，使用逻辑约束求解问题实现解的存在与否，可以编码到各种满足性求解器中，可用于合成和性能评估。

    Mar, 2018

  • 布尔函数综合的难点

    通过两阶段算法求解 Boolean functional synthesis，在满足一定条件下的第一阶段可提供正确答案，若不满足条件则第二阶段需通过指数级时间生成指数大小的函数，实验表明算法比现有技术更优秀。

    Apr, 2018

  • 布尔函数综合的知识编译

    研究 Boolean functional synthesis 问题中 CNF 转化为 SynNNF 的算法，并证明 SynNNF 具有多项式时间综合的优势。

    Aug, 2019

  • 有限合成的编码

    该研究探讨了将线性时间临时逻辑中的有界综合问题转化为布尔公式（SAT）、量化布尔公式（QBF）和依赖量化布尔公式（DQBF）的约束系统的问题，并通过反应综合竞赛（SYNTCOMP）和最先进的求解器对编码进行了系统评估，发现 QBF 的效果优于 SAT 和 DQBF。

    Mar, 2018

  • 使用答案集规划从生物动力学约束合成布尔网络

    该论文讨论了如何从有关域的限制和结果网络的动态属性中合成布尔函数。使用答案集编程来解决合成问题，然后对其解集进行非冗余特征描述。该方法的可扩展性通过随机网络的案例研究得到了展示，最多可达 100 到 1,000 节点，具备处理细胞分化过程细胞学建模的优势。

    Sep, 2019

  • 基于数据驱动的布尔函数合成方法 Manthan

    Manthan 是一种基于数据驱动的方法，将布尔函数综合视为分类问题，依赖于约束采样和自动推理等技术，通过对 609 个基准测试案例的评估，证明了其在现有技术上的显著改进，解决了当前技术不能解决的 60 个基准测试案例。

    May, 2020

  • BLASYS：使用布尔矩阵分解的近似逻辑综合

    该论文提出了一种新的用于综合近似电路的技术，采用布尔矩阵分解对电路子电路的真值表进行逼近，以获取更低复杂度的子电路，实验表明此方法可在不影响准确度的情况下，节约高达 63% 的功耗。

    May, 2018

  • 最佳优先自顶向下的程序合成

    该论文通过引入一种名为 Bee Search 的新的最佳优先从底向上搜索算法，解决了现有的基于成本指导的底向上搜索算法在信息损失和成本函数排序方面的问题。实证结果表明，Bee Search 在更复杂的领域特定语言（DSLs）中优于现有的成本指导的 BUS 算法，在简单的 DSLs 中与先前的方法表现相当好。此外，我们的新成本函数在字符串操作任务上优于先前的成本函数。

    Oct, 2023

  • FourierSAT: 一个基于傅里叶展开的代数框架求解混合布尔约束问题

    FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

    Dec, 2019

  • 显式依赖合成

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

    Jan, 2023