基于SAT问题实例特性的端到端SAT求解模型  

End-to-end SAT assignment model based oninstance related characteristics of SAT

作　　者：龙峥嵘 李金龙[1] 梁永濠 Long Zhengrong;Li Jinlong;Liang Yonghao(School of Computer Science&Technology,University of Science&Technology of China,Hefei 230026,China)

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026

出　　处：《计算机应用研究》2024年第11期3376-3381,共6页Application Research of Computers

摘　　要：当前基于神经网络的端到端SAT求解模型在各类SAT问题求解上展现了巨大潜力。然而SAT问题难以容忍误差存在,神经网络模型无法保证不产生预测误差。为利用SAT问题实例特性来减少模型预测误差,提出了错误偏好变量嵌入架构(architecture of embedding error-preference variables, AEEV)。该架构包含错误偏好变量嵌入调整算法和动态部分标签训练模式。首先,为利用参与越多未满足子句的变量越可能被错误分类这一特性,提出了错误偏好变量嵌入调整算法,在消息传递过程中根据变量参与的未满足子句个数来调整其嵌入。此外,提出了动态部分标签监督训练模式,该模式利用了SAT问题实例的变量赋值之间存在复杂依赖关系这一特性,避免为全部变量提供标签,仅为错误偏好变量提供一组来自真实解的标签,保持其他变量标签为预测值不变,以在训练过程管理一个更小的搜索空间。最后,在3-SAT、k-SAT、k-Coloring、3-Clique、SHA-1原像攻击以及收集的SAT竞赛数据集上进行了实验验证。结果表明,相较于目前较先进的基于神经网络的端到端求解模型QuerySAT,AEEV在包含600个变量的k-SAT数据集上准确率提升了45.81%。Recently,the neural network-based end-to-end SAT solver shows great potential in predicting the solution of SAT instances.However,SAT solvers do not accept any error,and the prediction error of neural network-based models is not inevitable.Aiming at the problem of the SAT does not allow for errors,this paper proposed an error preference variable embedding adjustment algorithm and a dynamic partial label supervised training mode to reduce the model prediction error by exploiting the properties of the SAT instance.Firstly,to take advantage of the characteristic that the more unsatisfied clauses a variable participates in,the more likely it was to be misclassified,this paper proposed an error preference variable embedding adjustment algorithm,which was used during the message passing process to adjust the embedding of a variable according to the number of unsatisfied clauses it participates in.In addition,this paper proposed a dynamic partial label supervised training mode,which exploited the feature of complex dependencies among variable assignments for SAT instances,avoiding to provide labels for all the variables,and providing only a set of labels from a solution for the error-preference variables,and keeping the other variables’label as the predictions unchanged,which managed a smaller search space during the training.Finally,this paper presented experimental validation on 3-SAT,k-SAT,k-Coloring,3-Clique,SHA-1 pre-image attack,and the collected SAT competition dataset.The results show that compared to the SOTA end-to-end model QuerySAT,AEEV improves the accuracy by 45.81%on the k-SAT dataset with 600 variables.

关 键 词：布尔可满足性问题 消息传递网络 机器学习 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]