计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答...计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming,ASP)求解器计算其稳定模型回答集.针对计算CNF公式的极小模型的问题,提出一种基于可满足性问题(satisfiability problem,SAT)求解器的计算极小模型的方法MMSAT;然后结合最近基于极小归约的极小模型验证算法CheckMinMR,提出了基于极小模型分解的计算极小模型方法MRSAT;最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明:MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的,且计算极小模型的速度都明显快于最新版的clingo,并且在SAT工业实例上发现了clingo有计算出错的情况,而MMSAT和MRSAT则更稳定.展开更多
在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(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倍左右.展开更多
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.展开更多
文摘计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming,ASP)求解器计算其稳定模型回答集.针对计算CNF公式的极小模型的问题,提出一种基于可满足性问题(satisfiability problem,SAT)求解器的计算极小模型的方法MMSAT;然后结合最近基于极小归约的极小模型验证算法CheckMinMR,提出了基于极小模型分解的计算极小模型方法MRSAT;最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明:MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的,且计算极小模型的速度都明显快于最新版的clingo,并且在SAT工业实例上发现了clingo有计算出错的情况,而MMSAT和MRSAT则更稳定.
文摘在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(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.
