基于SAT的GRANULE算法不可能差分分析

基于布尔可满足性问题(SAT)的自动化搜索方法可以直接刻画与、或、非、异或等逻辑运算,从而建立更高效的搜索模型。为更高效地评估GRANULE算法抵抗不可能差分攻击的能力,首先,基于S盒差分分布表性质优化S盒差分性质刻画的SAT模型;其次,对GRANULE算法建立基于比特的不可能差分区分器的SAT模型,通过求解模型得到多条10轮GRANULE算法的不可能差分区分器;再次,针对不可能差分区分器,给出改进的SAT自动化验证方法并验证;最后,将得到的区分器往前和往后各扩展3轮,对GRANULE-64/80算法发起16轮的不可能差分攻击,通过该攻击可以恢复80比特主密钥,时间复杂度为251.8次16轮加密,数据复杂度为241.8个选择明文。与表现次优的对GRANULE算法不可能差分分析的方法相比,所得到的区分器轮数和密钥恢复攻击轮数都提高了3轮,且时间复杂度、数据复杂度都进一步下降。

基于多样性SAT求解器和新颖性搜索的软件产品线测试

软件产品线测试是一项非常具有挑战性的工作.基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的.因其具有良好的可拓展性和较好的测试效果,目前已成为软件产品线测试的重要手段之一.在该测试方法中,如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题.针对以上问题,提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search,NS)的软件产品线测试算法.具体地,所提算法同时采用两类多样性SAT求解器产生多样化的测试用例.特别地,为了改善随机局部搜索SAT求解器的多样性,提出一种基于概率向量的通用策略产生候选解.此外,为同时维护测试集的全局和局部多样性,设计并运用两种基于NS算法思想的归档策略.在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性,以及所提算法较其他主流算法的优越性.

SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION

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求解器算法的组合电路等价性检查研究

随着工艺节点的缩小,集成电路规模的增加,集成电路设计过程中逻辑等价性检查在确保设计功能正确性方面起着重要作用。文章研究了组合电路逻辑等价性检查技术,针对该领域常用的DPLL和CDCL算法存在的问题,提出了一种基于蒙特卡洛树搜索的改进算法。通过对ISCAS85测试集的一个子集的实验,证实该算法对CDCL算法有一定的改进,应用于组合电路等价性检查的平均运行时间减少了20%。

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

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

并行蚁群算法求解加权MAX-SAT

为了使得算法对蚁群进化的控制更加直接、算法更加高效,针对加权MAX-SAT的特点,以重离散化方式简化蚁群算法模型,提出取值概率的概念,并以之替换传统蚁群算法中信息素,最后对该算法作并行化改进。实验结果表明,得到的基于改进后并行化的蚁群算法更具有效性,搜索时间明显降低,取得了较好的加速比和效率。

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

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

求解恰当可满足性问题的随机局部搜索算法

可满足性问题(SAT)是一种NP完全问题,被广泛运用于人工智能和机器学习等研究。恰当可满足性问题(XSAT)是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面,对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题,分析了基础编码和等价编码两种转化方式的公式的部分性质,提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定;其次加入变元所属文字的恰当不可满足计分值,优先处理不易恰当满足的变元;然后使用防重复选择翻转变元的启发式策略减小搜索空间;最后,采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时,相较于ProbSAT,WalkXSAT的变元翻转次数与求解时间显著减少;在求解基础编码转化后的实例中,当实例变元规模大于100时,ProbSAT已失效,而WalkXSAT依然能够在短时间内求解。实验结果表明,所提WalkXSAT精确性高、稳定性强、收敛快。

SAT问题求解器重启策略对比分析

已有研究表明,在SAT求解器中引入重启可以极大地提高求解性能,并已出现了许多不同重启策略.目前还缺少全面的对比分析研究.为了避免重启策略选择的随意性,同时启发设计更好的重启策略,本文选择了具有代表性的7种重启策略,以目前广泛采用的Minisat为基本求解器,在国际SAT2011竞赛中实际应用类基准测试集之上进行了实验对比分析.结果表明:(1)不同重启策略对SAT求解器的求解过程和求解性能影响巨大;(2)在应用类测试集上,几何序列调度策略的平均综合性能优于其他策略;(3)在限定范围内,重启频率越大,求解器综合性能越好;(4)增量变化的重启频率可以克服固定重启频率导致不完备搜索的问题.

随机正则(k,r)-SAT问题的可满足临界

研究k-SAT问题实例中每个变元恰好出现r=2s次,且每个变元对应的正、负文字都出现s次的严格随机正则(k,r)-SAT问题.通过构造一个特殊的独立随机实验,结合一阶矩方法,给出了严格随机正则(k,r)-SAT问题可满足临界值的上界.由于严格正则情形与正则情形的可满足临界值近似相等,因此得到了随机正则(k,r)-SAT问题可满足临界值的新上界.该上界不仅小于当前已有的随机正则(k,r)-SAT问题的可满足临界值上界,而且还小于一般的随机k-SAT问题的可满足临界值.因此,这也从理论上解释了在相变点处的随机正则(k,r)-SAT问题实例通常比在相应相变点处同规模的随机k-SAT问题实例更难满足的原因.最后,数值分析结果验证了所给上界的正确性.

一种求解难SAT问题的改进DP算法

DP算法是求解SAT问题的最有效完全算法之一 ,论文分析和讨论了DP算法中的各种分枝文字策略 .并基于对不满足解数估计的方法 ,提出了一个有效的分枝文字策略 .实验结果表明 ,提出的改进DP算法对难SAT实例有较好的平均性能 .

可满足性模理论综述

可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。

MiniSAT求解器在电路故障诊断中的应用

MiniSAT求解器运用到电路故障诊断系统时,能够将判断一个电路是否存在故障问题转换为可满足性问题。本文将全加器的行为模型及观测分别使用合取范式(CNF)形式文件描述,调用MiniSAT求解器判定可满足性。该方法自动化程度高,能处理大规模的运算电路,具有较强的查找错误能力。

基于粗糙集和SAT算法的属性约简

粗糙集理论是80年代初由波兰数学家Z.Pawlak首先提出的一个分析数据的数学理论。该理论近几年来日益受到各领域的广泛关注,并已在机器学习、模式识别、决策分析、过程控制、数据库知识发现等广泛领域得到成功应用。论文提出了一种求最小约简的基于命题可满足性(简称SAT)算法的算法,提出一个解决SAT问题的分割和结合的算法。实验结果表明,论文所提算法在高度准确分类的基础上,所得约简中大大减少了规则的数目。

基于动态奖惩的分支策略的SAT完备算法

针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略。首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元。在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7。实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2%~29.3%,少数算例剪枝率的提高可达51%,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7%以上。所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间。

基于海明距的改进免疫算法及其在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则更稳定.

基于混合蚁群遗传算法的SAT问题求解

根据SAT问题的特点,通过分析传统蚁群算法和遗传算法在求解SAT问题上的不足,提出一种基于混合蚁群遗传算法的SAT问题求解方法。给出一种新的初始解的生成方式;在迭代过程中,根据较优解的累积信息提出进化算子;利用当前得到的最优解,通过改变不满足子句中文字的取值,增加变异算子。最后选取标准测试集中的20个实例对算法进行测试,实验结果表明:改进后的算法通常仅通过较少次数的迭代就能找到解,能够有效避免蚁群算法和遗传算法过早收敛的缺点,具有较强的寻优能力。

基于粗糙集和SAT的属性约简

属性约简是数据挖掘中的一种粗糙集方法,它决定了能代表整个信息系统的重要属性的集合。本文提出了一种求最小约简的基于命题可满足性(简称SAT)的算法,提出一个解决SAT问题的分割和结合的算法。实验结果表明,本文所提算法在高准确分类的基础上,在所得约简中大大减少了规则的数目。

一种规约于可满足性问题(SAT)的知识推理算法

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸。文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD。实验结果证实了这种方法的有效性。