一种可扩展且近乎均匀的 SAT 证明生成器
本文提出了一种基于算法的方法来解决 “几乎均匀地生成大型布尔约束条件的解” 的问题，该算法在解的均匀性方面提供了强大的理论保证，并可适用于涉及数十万个变量的问题。
Mar, 2014
提出使用有限独立哈希的新方法来解决 boolean satisfiability 问题，并基于此方法设计了两个实用算法：一个近似均匀生成器和一个可扩展的近似模型计数器，该方法具有强大的理论保证和可扩展性，可适用于不同的应用领域。
Apr, 2014
本文介绍一种名为基于覆盖率反馈的测试选择的自动约束提取和测试选择的新方法，通过选择具有高概率增加功能覆盖率的测试，有助于减少手动约束编写，优先考虑有效测试，降低验证资源消耗，加速大型工业硬件设计的覆盖率闭合。
May, 2022
通过系统的约束求解器的黑盒方案，结合搜索空间的统一探索，我们提出了一种新的采样技术，可以克服采样过程中的诸多困难，形成了自然的近似模型计数技术。
Oct, 2012
本文探讨了一种利用通用哈希和 SAT 求解器的方法，可以在不牺牲正确性保证的同时，处理具有数十万个变量的公式，解决了人工智能中受限采样和计数的两个基本问题，这对于概率推理及规划，约束随机验证等方面有着广泛应用，并探讨一些需要解决的挑战。
Dec, 2015
我们提出了一种新的高级综合方法，利用大型语言模型工具生成硬件设计。该方法仅使用开源工具，不包括大型语言模型。通过一个案例研究，我们使用该方法生成了一个具有 wishbone 接口的置换同余随机数生成器设计。我们使用大型语言模型生成的仿真和 Dieharder 随机性测试套件验证了随机数生成器设计的功能和质量。我们记录了案例研究中使用的所有大型语言模型聊天记录、Python 脚本、Verilog 脚本和仿真结果。我们相信，我们的硬件设计生成方法与开源硅 130 纳米设计工具相结合，将彻底改变应用特定集成电路设计。我们的方法大大降低了构建物联网领域特定计算加速器和概念验证原型的门槛，以后可以在更现代的工艺节点进行制造。
Nov, 2023
应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 10,000 个变量的公式的可满足性，提出了新的分类器，可以对大多数困难水平的相同数据集进行显着改进，从而打破了过去基于公式的句法特征学习的方法，并使用求解器计算的简短前缀进行学习。
Nov, 2022