标题： MILP-SAT-GNN：另一个神经SAT求解器 显示英文标题

标题： MILP-SAT-GNN: Yet Another Neural SAT Solver

摘要： 我们提出了一种新方法，通过利用一种用于将图神经网络（GNNs）应用于混合整数线性规划（MILP）的技术，使图神经网络（GNNs）能够解决SAT问题。 具体来说，k-CNF公式被映射到MILP问题，然后被编码为加权二分图，并随后输入到GNN中进行训练和测试。 从理论角度来看：(i) 我们建立了排列和等价不变性结果，证明该方法产生的输出在子句和变量重新排序下是稳定的；(ii) 我们识别出一个理论限制，表明对于一类称为可折叠公式的公式，标准GNN无法始终区分可满足和不可满足实例；(iii) 我们证明了一个通用逼近定理，确立了在随机节点初始化（RNI）下，该方法可以在有限数据集上以任意精度逼近SAT求解，即GNN在这种数据集上变得近似正确和完整。 此外，我们表明对于不可展开的公式，无需RNI即可实现相同的逼近保证。 最后，我们对我们的方法进行了实验评估，结果表明，尽管神经架构简单，该方法取得了有希望的结果。 显示英文摘要

摘要： We proposes a novel method that enables Graph Neural Networks (GNNs) to solve SAT problems by leveraging a technique developed for applying GNNs to Mixed Integer Linear Programming (MILP). Specifically, k-CNF formulae are mapped into MILP problems, which are then encoded as weighted bipartite graphs and subsequently fed into a GNN for training and testing. From a theoretical perspective: (i) we establish permutation and equivalence invariance results, demonstrating that the method produces outputs that are stable under reordering of clauses and variables; (ii) we identify a theoretical limitation, showing that for a class of formulae called foldable formulae, standard GNNs cannot always distinguish satisfiable from unsatisfiable instances; (iii) we prove a universal approximation theorem, establishing that with Random Node Initialization (RNI), the method can approximate SAT solving to arbitrary precision on finite datasets, that is, the GNN becomes approximately sound and complete on such datasets. Furthermore, we show that for unfoldable formulae, the same approximation guarantee can be achieved without the need for RNI. Finally, we conduct an experimental evaluation of our approach, which show that, despite the simplicity of the neural architecture, the method achieves promising results.