DeepSAT: 一种基于 EDA 驱动的 SAT 学习框架
本研究提出了 G2SAT 这一深度生成式框架,可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式,旨在扩展现有的数据集,为 SAT 求解器的性能提供优化方案。
Oct, 2019
EduSAT 是一个面向教育目的的教学工具,通过实现关键算法,支持学习和理解布尔可满足性和 SMT 求解技术,并提供了五个超越 SAT 和 SMT 的 NP 完全问题的求解器抽象。
Aug, 2023
本文提出了一种新的路线,即通过引入可微(平滑)的最大可满足性(MAXSAT)求解器,将逻辑推理纳入更大的深度学习系统的循环中,从而在端到端学习系统中学习有挑战性的问题的逻辑结构,表现出集成逻辑结构于深度学习的潜力。
May, 2019
使用去噪扩散和图神经网络生成多样化的布尔可满足性问题的解决方案,结果比现有最佳纯神经方法的准确度相似,即使系统用标准求解器中的非随机解进行训练,生成的解决方案也极其丰富。
Nov, 2022
通过三分图表示的实例和异构图神经网络模型,我们提出了一种基于 GraSS 的自动 SAT 求解器选择方法,该方法使用了特定领域决策,如新的节点特征设计、图中子句的位置编码、针对三分图的 GNN 架构以及运行时间敏感的损失函数,通过广泛的实验,我们证明了这种组合对于七种最先进的求解器来说在回路设计基准测试和 2022 SAT 大赛 20 年纪念赛道的实例中都能提高运行时间。
May, 2024
本文提出了基于 SAT 的方法学习最优二元决策图(BDD),以更好地实现可解释的机器学习模型,并给出了一种整合兼容子树的方法,该方法与现有方法相比在预测质量和可解释性方面具有明显的优势。
Mar, 2022
布尔可满足性 (SAT) 是一个基础的 NP-complete 问题,具有许多应用,包括自动计划和调度。为了解决大规模的情况,SAT 求解器必须依赖启发式算法,如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法,通过减少步数来降低运行时间,但是由于有用的模型相对较大和较慢,这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤,然后将控制权交给经典启发式算法,这简化了 SAT 求解的冷启动,并可以减少步数和总运行时间,但需要单独决定何时将控制权交给求解器。此外,我们介绍了一种改进的 Graph-Q-SAT,专门针对从其他领域转换而来的 SAT 问题,例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。
Jul, 2023
本研究提供了两个新的卫星数据集 SAT-4 和 SAT-6,以及一个卫星影像分类框架,该框架从输入图像中提取特征,将其标准化并将标准化的特征向量馈入深度置信网络进行分类。与其他算法相比,该方法在两个数据集上均表现优异,能有效地学习更好的卫星影像表现.
Sep, 2015