GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection

布尔可满足性（SAT）问题在现实应用中通常由SAT求解器解决，然而对于相同的实例，不同求解器的求解时间可能差异巨大。这促使人们研究机器学习模型，可以预测对于给定的SAT实例，在多个选项中选择哪个求解器。现有的SAT求解器选择方法都依赖于一些手动选择的实例特征，这些特征计算成本高昂，并忽略SAT图中的结构信息。本文提出了GraSS，一种基于三分图表示实例和异构图神经网络（GNN）模型的自动SAT求解器选择方法。虽然GNN在其他SAT相关任务中已被采用，但它们不包含任何领域特定的知识，并忽略了不同子句顺序引入的运行时变化。我们通过领域特定的决策，例如新的节点特征设计、图中子句的位置编码、适用于我们三分图的GNN架构和运行时敏感的损失函数，来丰富图表示。通过大量实验，我们证明了原始表示和领域特定选择的组合可以提高七个最先进求解器在工业电路设计基准测试和2022 SAT竞赛20周年纪念赛的实例上的运行时间。

自动SAT求解器选择问题

使用三分图表示SAT实例并结合领域知识和运行时敏感的损失函数，采用异构图神经网络模型进行SAT求解器选择，提高求解效率。

论文提出了一种基于三分图表示的SAT求解器自动选择方法，结合了领域知识和运行时敏感的损失函数，通过实验在工业电路设计基准测试和2022 SAT竞赛的20周年纪念赛实例上，对七种最先进的求解器进行了评估，取得了较好的效果。

最近相关研究包括基于特征工程的SAT求解器选择方法和基于深度学习的SAT相关任务，如基于图神经网络的SAT变量重要性评估和基于递归神经网络的SAT公式生成等。