使用SAT求解器产生所有极小冲突部件集

产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效率进一步提高(平均提高约21%,最高者甚至达到约48%).

基于硬件可编程逻辑的SAT求解算法研究与进展

布尔可满足性SAT问题作为第一个被证明的NP完全问题,是计算机理论与应用的核心问题,有着重要的应用价值,因此近年来涌现了各种各样SAT求解器。但是,SAT求解器的运算效率始终是影响其应用的关键因素,所以利用硬件的高性能与并行性来加速SAT求解过程已成为验证领域的一个研究热点。归纳总结了在SAT求解过程中,利用硬件现场可编程门逻辑FPGA的并行性和灵活性加速求解过程的各种算法研究,着重总结分析了应用型SAT求解器的加速策略。通过对各种方法的深入分析,指出它们的优缺点,为未来的研究提供了思路。

基于SAT的路径规划系统的设计

本文主要介绍了基于SAT路径规划算法以及路径规划系统的设计方案。通过移动机器人抓取积木为例,介绍了基于SAT路径规划算法包括的规划问题的命题表示方法以及如何使用SAT求解器对规划命题进行求解。该系统较传统的路径规划系统而言,路径规划解提取速度较快,无需传感器的反复检测初始状态及目标状态,规划效率较高。

基于MiniSAT的命题极小模型计算方法

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正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则更稳定.

CDCLSAT求解器的重启策略分析

CDCL SAT求解器在形式验证等领域应用广泛,但重启策略众多且参数控制复杂,导致通常选择默认参数下的策略,从而降低求解器的效率和易用性.为了提高CDCL SAT求解器的实用性,通过实验分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响,以及求解初期的决策变量数等行为特征数据集与重启策略集之间的关系.实验结果表明,通过改变重启策略可以提高求解效率,所得到的最优解比缺省解的效率可提高6 959%,平均提高411%;重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性;相比重启频率,重启序列对求解效率影响更大.进一步用7种重启策略集合覆盖97%案列的最优重启策略,通过求解初期的特征值变化频率与相应的重启策略关联,为后期选择最优重启策略提供技术支持.

一种基于SAT求解器的组合电路重汇聚现象分析方法

为了研究组合电路重汇聚现象,提出了一种基于SAT求解器的分析方法。通过深度优先搜索算法,确定瞬态脉冲产生节点和输出节点之间的所有路径;建立待检查列表,对表中的元素施加敏化约束条件,并采用SAT求解器求解元素可满足性;最后判断是否存在满足条件的输入向量,使瞬态脉冲通过不同路径在输出节点发生重汇聚。所提方法可以有效地对较大规模组合电路进行分析,采用EPFL和ISCAS’85作为测试集,实验结果表明,ISCAS’85测试集中约有一半节点处产生的瞬态脉冲能够发生重汇聚,这一比例明显高于EPFL测试集,因此不同类型功能电路重汇聚现象的发生率存在较大差异。

基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器(GLUCOSE4.1并行版本)为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。

基于寻找可满足2-SAT子问题的SAT算法

可满足问题(SAT)是一个NP-Hard问题。提出了一种求解SAT的新算法(FFSAT)。该算法将SAT问题转换为寻找一个可满足的2-SAT子问题。SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解。使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题。实验结果表明,采用本算法的结果优于UnitWalk。

基于SAT的多目标故障测试向量动态压缩方法

针对传统的自动测试图形向量生成采用逐个求解单一故障模型导致生成测试向量数据量巨大的缺点,提出一种基于布尔满足性(boolean satisfiability,SAT)的多目标故障测试向量动态压缩方法,同时论证多目标故障测试生成问题为布尔满足性问题。该方法将具有鲁棒性的SAT算法嵌入经典的动态压缩流程中,首先利用经典动态压缩算法求解最小测试向量检测大部分失效故障,然后采用SAT求解器对未测出的多故障电路进行同一求解和附加约束求解方式,最终得到故障覆盖率高的测试向量和同一测试最大故障列表。实验数据表明,在相同电路模型情况下,此方法求得的测试向量相比经典动态压缩减少高达70%。

基于SAT的ARX不可能差分和零相关区分器的自动化搜索

ARX(Addition,Rotation,Xor)算法基于模整数加,异或加和循环移位三种运算,便于软硬件的快速实现.不可能差分分析和零相关分析是攻击ARX的有效方法,攻击的关键是搜索更长轮数、更多数量的不可能差分和零相关区分器.目前很多的搜索方法都没有充分考虑非线性组件的性质,往往不能搜索得到更好、更准确的区分器.本文提出了基于SAT(Satisfiability)的ARX不可能差分和零相关区分器的自动化搜索算法.通过分析ARX算法组件的性质,特别是常规模加和密钥模加这两种非线性运算差分和线性传播的特性,给出了高效简单的SAT约束式.在此基础上,建立SAT模型进行区分器的搜索.作为应用,本文首次给出了Chaskey算法13条4轮不可能差分和1条4轮零相关区分器;首次给出了SPECK32算法10条6轮零相关区分器和SPECK48算法15条6轮零相关区分器;在较短的时间内,给出了HIGHT算法17轮的不可能差分和零相关区分器.与现有结果相比,无论是区分器的条数,还是搜索区分器的时间均有明显的提升.此外,通过重新封装求解器STP的输出接口,建立了自动化的SAT\\SMT分析模型,能够给出ARX算法在特殊输入输出差分和掩码集合下,不可能差分和零相关区分器轮数的上界.

基于SAT方法进一步加速差分特征的搜索

回顾了孙等使用Matsui边界条件加速差分特征搜索的方法,为了进一步提高搜索效率,改进了Matsui边界条件以及利用Matsui边界条件加速差分特征自动化搜索的方法,并提出了一种改进的方法来搜索分组密码的最优差分特征。研究了线程数和询问条件的加速效果并提出了选择线程数以及询问条件的策略。使用STP和CryptoMiniSat分别搜索概率为2^(-24)、2^(-25)、2^(-26)的8轮SPECK96差分特征以及概率为2^(-39)的11轮HIGHT差分特征,并比较了在不同线程数和询问条件下求解SAT/SMT问题的耗时。研究发现线程数对搜索差分特征的耗时影响较大,而询问条件对搜索差分特征的耗时影响较小,从而提出了一种如何选择线程数和询问条件的策略。根据所提策略,使用改进的边界条件和方法搜索HIGHT的11轮最优差分特征,并首次获得了HIGHT的11轮最优差分特征的紧致概率,即2^(-45)。现有的11轮HIGHT最优差分特征概率的最紧致边界是P_(Opt)^(11)≥2^(-45)。这就意味着,利用现有11轮HIGHT最优差分特征概率的最紧致边界无法给出11轮HIGHT抗差分分析安全性的精确评估。因此,所提策略的结果是目前已知的最优结果。

基于不可满足核的近似逼近可达性分析

近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.研究并提出了一种新的模型检测技术,可以有效地对迁移系统进行模型检测,包括不安全性检测和证明安全性.与现有的模型检测算法不同,提出的基于不可满足核(unsatisfied core,UC)的近似逼近可达性分析(UC-based approximate incremental reachability,UAIR),主要利用不可满足核来求解一系列的候选安全不变式,直至生成最终的不变式,以此来实现安全性证明和不安全性检测(漏洞查找).在基于SAT求解器的符号模型检测中,使用由可满足性求解器得到的UC构造候选安全不变式,如果迁移系统本身是安全的,得到的初始不变式只是安全不变式的一个近似.然后,在检查安全性的同时,逐步改进候选安全不变式,直到找到一个真正的不变式,证明系统是安全的;如果系统是不安全的,该方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法,利用不可满足核进行安全性模型检测,取得了相当好的效果.众所周知,模型检测领域没有绝对最好的方法,尽管该方法在基准的可解数量上无法超越当前的成熟方法,例如IC3,CAR等,但是该方法可以解出3个其他方法都无法解出的案例,相信本方法可以作为模型检测工具集很有价值的补充.

基于模型诊断中结合问题特征的新方法

基于模型诊断一直是人工智能领域中热门的研究问题.近些年来,随着SAT求解器效率的逐渐提高,基于模型的诊断也被转换成SAT问题进行求解.在对基于模型诊断求解方法 CSSE-tree深入研究基础上,结合诊断问题和SAT求解过程的特征,给出先对包含组件个数较多的候选诊断进行求解的方法,进而减小SAT求解问题的规模;在对极小诊断解和非极小诊断解剪枝方法的基础上,首次提出非诊断解定理及非诊断解空间的剪枝方法,有效地实现了对诊断的无解空间进行剪枝.根据组件个数较多的候选诊断先求解及有解无解剪枝方法特征,构建基于反向搜索的LLBRS-tree方法.实验结果表明:与CSSE-tree算法相比,LLBRS-tree算法减少了SAT求解次数、减小了求解问题规模,效率较好,尤其是求解多诊断时效率提高更为显著.

使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的.

使用布尔可满足性的组合电路等价性验证算法

该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了'与／非'图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆 炸,推理简化减小了SAT搜索空间。ISCAS85电路实验结果表明了本算法的有效性。

具有约束条件的组合测试用例集的构建方法

针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解器进行求解,找出满足约束条件的约束组合测试用例。最后运用AETG-SAT算法得到较优的组合测试用例集,并通过实验表明了AETG-SAT算法的优越性。

基于可满足性问题求解器的星上FPGA永久损伤容错技术研究

现代卫星广泛使用的FPGA在空间高能粒子的影响下,会产生门电路的永久性损伤。而传统的三模冗余等容错方法不但成倍增加了系统硬件开销,还存在因冗余器件耗尽而失效的风险。因此,提出一种利用FPGA自身冗余资源,修复永久性损伤的容错方案。该方案通过建立FPGA内部资源的功能模型,将容错问题转化为数学上的可满足性问题。并且利用经过改进的GSAT算法对该问题求解,可以获得在功能上与损伤前完全相同的电路结构,及其所对应的FPGA配置文件。将该文件重新下载到FPGA中,可以屏蔽损伤带来的影响,从而达到利用FPGA自身冗余资源容错的目的。通过实验和分析可以看出,本文方案具有对损伤修复成功率高、计算量小和需要内存空间少的特点,因此符合星上计算能力和硬件资源十分有限的实际情况。

语义标识的过程模型的可执行性分析

语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型的动态语义;定义了该动态语义的命题公式的编码规则;提出了基于可满足性求解器的可执行性分析方法;该方法能判定可执行性问题同时当模型不满足可执行性时能反馈出有问题的活动;此外,实现了相应的原型工具SPMT,该工具支持对语义过程模型的建模及可执行性分析;最后通过实际例子对以上理论及工具进行了有效性验证.

结合问题特征的分组式诊断方法

模型诊断方法是人工智能领域重要的系统故障自动检测方法,被广泛应用于软件故障检测和硬件诊断.近年来由于电路规模和复杂度不断增大,其诊断难度也不断增大.本文通过对电路模型特征的研究,结合LLBRStree(Last-Level Based on Reverse Search-tree)诊断算法提出分组式诊断方法 GD(Grouped Diagnosis):首先结合电路特征确定组件的故障相关性并对电路组件进行分组,可缩减电路中需检测的规模;其次,利用分组后电路并结合非诊断解定理和SAT(SATisfiability)求解特征定位部分非诊断解,从而避免该部分的一致性检测来加速求解.本文算法可应用于电子电路故障诊断领域,并且实验结果表明该算法与LLBRS-tree算法相比求解效率平均提高了1.5倍,最多提高了3倍.

针对PRESENT分组密码算法的代数分析

研究针对PRESENT分组密码的代数分析。通过使用S盒的表达式形式,构建出多轮PRESENT加密中的代数方程组。这种构建方程的方法被推广到具有小型S盒的典型SPN型分组密码算法的方程构建问题中。对简化的PRESENT算法进行了攻击实验,采用MiniSAT作为攻击过程中的求解工具,对四轮、六轮PRESENT加密进行实际攻击。可以在1 min内恢复四轮加密的所有密钥,数小时内恢复六轮加密的密钥。通过引入了差分思想,将有效攻击轮数提高到八轮。