As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the ...As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.展开更多
当前基于神经网络的端到端SAT求解模型在各类SAT问题求解上展现了巨大潜力。然而SAT问题难以容忍误差存在,神经网络模型无法保证不产生预测误差。为利用SAT问题实例特性来减少模型预测误差,提出了错误偏好变量嵌入架构(architecture of ...当前基于神经网络的端到端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%。展开更多
This paper reviews the recent literature on solving the Boolean satisfiability problem(SAT),an archetypal N P-complete problem,with the aid of machine learning(ML)techniques.Over the last decade,the machine learning s...This paper reviews the recent literature on solving the Boolean satisfiability problem(SAT),an archetypal N P-complete problem,with the aid of machine learning(ML)techniques.Over the last decade,the machine learning society advances rapidly and surpasses human performance on several tasks.This trend also inspires a number of works that apply machine learning methods for SAT solving.In this survey,we examine the evolving ML SAT solvers from naive classifiers with handcrafted features to emerging end-to-end SAT solvers,as well as recent progress on combinations of existing conflict-driven clause learning(CDCL)and local search solvers with machine learning methods.Overall,solving SAT with machine learning is a promising yet challenging research topic.We conclude the limitations of current works and suggest possible future directions.The collected paper list is available at https://github.com/ThinklabSJTU/awesome-ml4co.Keywords:Machine learning(ML),Boolean satisfiability(SAT),deep learning,graph neural networks(GNNs),combinatorial optimization.展开更多
在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(degree of element coverage,DOEC)极小化策略的SAT求解极小碰...在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(degree of element coverage,DOEC)极小化策略的SAT求解极小碰集的方法 SAT-MHS(satisfiability problemminimal hitting sets).首先,方法SAT-MHS将碰集求解问题转换成SAT问题,即把所有的冲突集合以子句形式表示成SAT的输入CNF进行迭代求解.其次,提出比现有的基于子超集检测极小化策略(sub-superset detecting minimization,SSDM)更为高效的DOEC极小化策略进行极小化处理.由实验数据可见,与SSDM极小化策略相比,其优点是缩减了求解空间和迭代求解次数,尤其当求解规模较大问题时,其极小化效率越高.主要是因为其极小化不会随着待求解问题规模的增加而增加,而是只与冲突集合簇的大小相关,因此时间复杂度较低.实验结果表明,对于一些较大的实例,与目前效率最好的Boolean方法相比,SAT-MHS方法高效且易于实现,求解速度能提高10～20倍,DOEC极小化策略对比传统SSDM极小化策略能达到40倍左右.展开更多
基金Supported by the National Natural Science Foundation of China(Nos.61063002,61100186,61262008)Guangxi Natural Science Foundation of China(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220)the Key Project of Education Department of Guangxi
文摘As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.
基金supported by National Key Research and Development Program of China(No.2020AAA0107600)National Science Foundation of China(No.62102258)+2 种基金Shanghai Pujiang Program,China(No.21PJ1407300)Shanghai Municipal Science and Technology Major Project,China(No.2021SHZDZX0102)Science and Technology Commission of Shanghai Municipality Project,China(No.22511105100),and also sponsored by Huawei Ltd,China.
文摘This paper reviews the recent literature on solving the Boolean satisfiability problem(SAT),an archetypal N P-complete problem,with the aid of machine learning(ML)techniques.Over the last decade,the machine learning society advances rapidly and surpasses human performance on several tasks.This trend also inspires a number of works that apply machine learning methods for SAT solving.In this survey,we examine the evolving ML SAT solvers from naive classifiers with handcrafted features to emerging end-to-end SAT solvers,as well as recent progress on combinations of existing conflict-driven clause learning(CDCL)and local search solvers with machine learning methods.Overall,solving SAT with machine learning is a promising yet challenging research topic.We conclude the limitations of current works and suggest possible future directions.The collected paper list is available at https://github.com/ThinklabSJTU/awesome-ml4co.Keywords:Machine learning(ML),Boolean satisfiability(SAT),deep learning,graph neural networks(GNNs),combinatorial optimization.
文摘在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(degree of element coverage,DOEC)极小化策略的SAT求解极小碰集的方法 SAT-MHS(satisfiability problemminimal hitting sets).首先,方法SAT-MHS将碰集求解问题转换成SAT问题,即把所有的冲突集合以子句形式表示成SAT的输入CNF进行迭代求解.其次,提出比现有的基于子超集检测极小化策略(sub-superset detecting minimization,SSDM)更为高效的DOEC极小化策略进行极小化处理.由实验数据可见,与SSDM极小化策略相比,其优点是缩减了求解空间和迭代求解次数,尤其当求解规模较大问题时,其极小化效率越高.主要是因为其极小化不会随着待求解问题规模的增加而增加,而是只与冲突集合簇的大小相关,因此时间复杂度较低.实验结果表明,对于一些较大的实例,与目前效率最好的Boolean方法相比,SAT-MHS方法高效且易于实现,求解速度能提高10～20倍,DOEC极小化策略对比传统SSDM极小化策略能达到40倍左右.
