布尔函数综合的知识编译
通过两阶段算法求解 Boolean functional synthesis，在满足一定条件下的第一阶段可提供正确答案，若不满足条件则第二阶段需通过指数级时间生成指数大小的函数，实验表明算法比现有技术更优秀。
Apr, 2018
研究了没有语言文法限制的综合技术，证明它可以被约化为 DQF 问题，通过 DQF 求解来设计综合程序并且克服了基于文法的综合技术的限制，实现了更好的性能。
May, 2021
该研究提出一种名为 Manthan3 的数据驱动的方法，用于解决依赖量化布尔公式中的 Henkin 合成问题，实现对线路的验证、控制器合成和线路实现等应用方面具有积极的意义。
Jan, 2023
该论文介绍了一种名为 BNSynth 的工具，它是解决具有解决方案空间范围限制的 BFS 问题的第一个工具，该工具利用反例指导的神经方法去综合较小的函数，并且相比现有的工具，平均方案大小减少了至少 3.2 倍（最高可达 24 倍）。
Dec, 2022
该研究旨在解决将命题公式转化为任意格式的等价公式的问题，使用量子布尔公式编码的方法可以有效地解决此类问题，因为这种方法远优于使用暴力方法或者 SAT 求解器进行转化。
Mar, 2023
FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。
Dec, 2019
本文介绍了可分解否定范式（DNNF）作为可行的命题理论形式，并提供了一些在多项式时间内可以执行的强大逻辑操作。在此基础上，本文提出了将任何合取范式（CNF）转化为 DNNF 的算法，并提供其空间和时间复杂度上的结构保证。同时它也介绍了将有序二叉决策图（OBDD）表示的命题理论转换为等价的 DNNF 的线性时间算法。接着，介绍了采用新的操作在 d-DNNF 上遍历之后实现线性时间、完整的信念修正系统。
Mar, 2000
本研究提出了 G2SAT 这一深度生成式框架，可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式，旨在扩展现有的数据集，为 SAT 求解器的性能提供优化方案。
Oct, 2019