基于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求解器

针对布尔可满足性问题的高效求解进行了研究。首先,通过对k-SAT问题和基于耦合常微分方程形式的确定性连续时间动态系统的分析,提出了一种基于时延信息形式的改进连续时间动态系统方程,以保持集中搜索特性;然后,提出了实现该系统方程的三个主要组件即信号动态电路、辅助变量电路和数字验证电路的模拟设计。在信号动态电路的设计中,设计了一种获得更高性能、更小面积和更低功耗的模拟硬件形式;在提出的辅助变量电路和数字验证电路的模拟硬件设计中,实现了避免梯度下降搜索陷入无解和确定给定问题的解是否已经找到的目标;同时提出了降低面积和功耗的可替代辅助变量电路的两种设计方案。仿真实验结果表明,提出的新的模拟SAT求解器不仅是有效的,而且相比于单一软件算法实现的SAT求解器和其他硬件类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)是一种NP完全问题,被广泛运用于人工智能和机器学习等研究。恰当可满足性问题(XSAT)是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面,对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题,分析了基础编码和等价编码两种转化方式的公式的部分性质,提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定;其次加入变元所属文字的恰当不可满足计分值,优先处理不易恰当满足的变元;然后使用防重复选择翻转变元的启发式策略减小搜索空间;最后,采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时,相较于ProbSAT,WalkXSAT的变元翻转次数与求解时间显著减少;在求解基础编码转化后的实例中,当实例变元规模大于100时,ProbSAT已失效,而WalkXSAT依然能够在短时间内求解。实验结果表明,所提WalkXSAT精确性高、稳定性强、收敛快。

基于SAT的安全协议惰性形式化分析方法

提出了一种基于布尔可满足性问题的安全协议形式化分析方法 SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此方法实现了一个安全协议分析工具,针对Otway-Rees协议检测出了一种类型缺陷攻击;针对OAuth2.0协议,检测结果显示对现实中存在的一些应用场景,存在一种利用授权码截取的中间人攻击。

随机正则(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实例有较好的平均性能 .

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

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

基于聚类和划分的SAT分治判定

提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂问题分解为多个子问题来求解.这种分治判定方法一方面降低了原公式的可满足性判定复杂度;另一方面,由于子句组的判定可以并行,因而判定速度能够得到进一步的提高.对于不能直接产生布尔子句组划分的情形,提出了一种利用聚类技术将CNF公式聚类成多个簇,然后消去簇间的公共变量来产生子句组划分的方法.

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

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

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

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

基于海明距的改进免疫算法及其在SAT中的应用

免疫算法可以克服遗传算法的早熟和发散现象,是一种有效的全局寻优算法.针对传统基于信息熵的免疫算法的浓度计算中含有过多的对数计算,浪费了机时,影响了免疫算法效率的缺陷;本文提出了一种基于海明距与加速免疫进化的变异算子的改进免疫算法,证明了基于海明距与基于信息熵的浓度定义在控制中所起的作用是等效的,并将这种改进算法应用于SAT求解.实验结果表明,改进的免疫算法在求解速度,成功率等方面都有明显的改善.

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

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

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

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

H-GRASP:一种基于GRASP改进的混合SAT解法器

为了改善GRASP的局限性,提出了一种能解决含有伪布尔(PB)和合取范式(CNF)混合约束问题的新的混合算法(H-GRASP)。该新算法采用了切削平面技术来提取PB约束条件之间的推论,并把它结合到普通的蕴涵图中,分析引起冲突的学习。与解决混合约束问题的其他两种方法——整数线性规划和纯基于SAT方法进行了彻底的比较。实验结果证明,H-GRASP方法从整体上大大减少了运行时间,加快了速度,同时还保证了加入这种方法的低耗费。

基于SAT的电路错误定位方法研究进展

随着VLSI芯片复杂度不断增加,功能验证与调试已占到整个芯片设计周期的60%以上。而错误的定位往往消耗大量的时间与精力,因此迫切需要一种高效的方法诊断与定位电路中的错误。针对近年来出现的许多电路错误定位方法,介绍了电路错误诊断方法的分类与工作流程,深入分析了基于SAT的错误定位方法的基本原理;对各种算法进行了概述评论,并简要介绍了在不可满足子式求解方面所做的一些研究工作,而不可满足子式能够显著提高错误定位效率与精度;讨论了电路错误定位技术所面临的主要挑战,并对今后的研究方向进行了展望。

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

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