Apr, 2022

SATfeatPy：用于可满足性问题的基于 Python 的特征提取系统

PDF
TL;DR本文介绍了 SATfeatPy 这个 Python 库，该库可以对 CNF 格式的 SAT 问题进行特征提取，实现了该领域主要论文中所有的结构和统计特征，并使用该库从 3000 个 SAT 和 UNSAT 实例生成的五组特征对十种不同类型的问题进行了高准确度的 SAT/UNSAT 和问题类别分类。最后，在去除一些特征后，比较特征的实用性和对于预测 SAT 实例的原始结构的重要性。
feature extractionmachine learningsat solvingcnf instancessatfeatpy
发现论文，激发创造
  • Python 自动化特征工程与选择的 autofeat 库

    本文介绍了 Autofeat Python 库，该库能为 Scikit-Learn 风格的线性回归和分类模型提供自动特征工程和选择功能。通过多阶段的特征工程和选择过程，它可以生成一个非线性特征池，从中选择出一组有意义的特征来提高线性模型的预测准确率，同时保持其可解释性。

    Jan, 2019

  • 基于连接查询和约束求解的特征模型配置

    本文介绍了如何利用关系数据库系统支持的合取查询方法，解决约束满足问题和特征模型配置任务，从而将数据库技术应用于解决配置任务，并在识别和解决不一致性方面提供了新的算法方法。

    Apr, 2023

  • 一种增强特征提取器，用于约束求解器的组合

    本文介绍了一种取自不同建模语言（MiniZinc、FlatZinc 或 XCSP）的限制编程（CSP）问题的特征集，用于求解器选择，实验结果显示使用这些特征可与最先进的 CSP 投资组合技术相竞争

    Aug, 2013

  • 解决布尔可满足性问题的机器学习方法

    本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

    Mar, 2022

  • 监督式特征排名算法的新型评估方法

    本文提出了一种新的评估方法，使用合成数据集评估特征重要性得分，并构建了一个名为 fseval 的 Python 基准测试框架，该框架允许在 HPC 系统上并行和分布式地执行实验。通过与在线平台 Weights and Biases 集成，可以在实时仪表板上交互地探索图表。研究结论通过探索一种大规模实验来找出参与算法的优点和缺点。

    Jul, 2022

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

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

    Dec, 2019

  • SAT: 简单的实例自适应自训练提高半监督文本分类

    本文提出了一种简单的实例自适应自训练方法 (SAT)，用于半监督文本分类。SAT 通过生成两个扩充视图来识别伪标签并用于模型训练，实验结果表明 SAT 方法具有竞争力的性能。

    Oct, 2022

  • G2SAT：学习生成 SAT 公式

    本研究提出了 G2SAT 这一深度生成式框架，可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式，旨在扩展现有的数据集，为 SAT 求解器的性能提供优化方案。

    Oct, 2019

  • SATformer: 应用于 SAT 求解的 Transformer

    本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构以捕捉这些子句之间的关系，并注重没能同时出现在 UNSAT 核心中的子句的权重，实验结果表明，SATformer 能够优于现有的基于学习的 SAT 求解器。

    Sep, 2022

  • SAT 问题的机器学习：约束启发式和新的图表示

    布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法，通过减少步数来降低运行时间，但是由于有用的模型相对较大和较慢，这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤，然后将控制权交给经典启发式算法，这简化了 SAT 求解的冷启动，并可以减少步数和总运行时间，但需要单独决定何时将控制权交给求解器。此外，我们介绍了一种改进的 Graph-Q-SAT，专门针对从其他领域转换而来的 SAT 问题，例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。

    Jul, 2023