期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
有界模型检测的优化 被引量:10
1
作者 杨晋吉 苏开乐 +2 位作者 骆翔宇 林瀚 肖茵茵 《软件学报》 EI CSCD 北大核心 2009年第8期2005-2014,共10页
G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-... G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值. 展开更多
关键词 模型检测 有界模型检测 可满足性问题 模态算子 递推公式
下载PDF
可满足性问题的闭环DNA算法 被引量:8
2
作者 周康 魏传佳 +1 位作者 刘朔 王防修 《华中科技大学学报(自然科学版)》 EI CAS CSCD 北大核心 2009年第7期75-78,共4页
给出并证明了可满足性问题有解的一个充分必要条件,即合取范式的成假赋值仅由与简单析取式个数相等的有限个向量决定.在此条件基础上设计出用这些向量对初始赋值进行筛除的可满足性问题过滤算法,该算法的时间复杂性仅与向量个数和维数有... 给出并证明了可满足性问题有解的一个充分必要条件,即合取范式的成假赋值仅由与简单析取式个数相等的有限个向量决定.在此条件基础上设计出用这些向量对初始赋值进行筛除的可满足性问题过滤算法,该算法的时间复杂性仅与向量个数和维数有关.为了在DNA计算模型上实现可满足性问题过滤算法,采用2n维向量的数据结构进行DNA编码代表可满足性问题的赋值;而闭环DNA计算模型的删除实验恰好能够完成对初始赋值的筛选,得到可满足性问题的可行解.最后用闭环DNA计算模型实现了可满足性问题过滤算法,并用实例说明了算法的有效性和可行性. 展开更多
关键词 可满足性问题 闭环DNA计算模型 过滤算法 删除实验 接入实验
原文传递
求解可满足性问题全部解的改进多种群克隆免疫算法
3
作者 张英杰 范朝冬 《信息与控制》 CSCD 北大核心 2011年第1期34-38,共5页
对于可满足性问题全部解(ALLSAT问题)的求解而言,随着问题规模增大,现有算法逐渐变得不适用.针对不能有效求解ALLSAT问题的现状,提出了一种多种群克隆免疫算法,该算法采用小生境方法和位爬山算法进行优化,维持种群多样性,提高算法收敛... 对于可满足性问题全部解(ALLSAT问题)的求解而言,随着问题规模增大,现有算法逐渐变得不适用.针对不能有效求解ALLSAT问题的现状,提出了一种多种群克隆免疫算法,该算法采用小生境方法和位爬山算法进行优化,维持种群多样性,提高算法收敛速度进行了算法收敛性分析.ALLSAT问题的求解结果表明,该算法是非常有效的. 展开更多
关键词 可满足性问题 多种群 克隆免疫算法 位爬山算法 小生境
下载PDF
基于OpenMP的并行遗传算法求解SAT问题 被引量:6
4
作者 吴贯锋 徐扬 +2 位作者 常文静 陈树伟 徐鹏 《西南交通大学学报》 EI CSCD 北大核心 2019年第2期428-435,共8页
为了提高SAT (boolean satisfiability)问题求解效率,在OpenMP (open multi-processing)编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别.算法采用OpenMP中的编译... 为了提高SAT (boolean satisfiability)问题求解效率,在OpenMP (open multi-processing)编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别.算法采用OpenMP中的编译制导语句#pragma omp parallel粗粒度并行化驱动混合遗传算法,采用#pragma omp single语句块实现了子种群间个体的同步迁移操作.与同类算法HCGA (hybrid cloud genetic algorithm)比较分析表明:改进算法HGA (hybrid genetic algorithm)以及并行后的混合遗传算法CGPHGA(coarse-grained parallel hybrid genetic algorithm)在求解成功率和求解效率上都有显著提高,部分问题求解成功率提高达5倍. 展开更多
关键词 sat问题 OPENMP 并行混合遗传算法 粗粒度模型
下载PDF
A Hopeful CNF-SAT─Algorithm Its High Efficiency, Industrial Application and Limitation
5
作者 黄文奇 李未 《Journal of Computer Science & Technology》 SCIE EI CSCD 1998年第1期9-12,共4页
From the SAT physical model, a physical hypothesis named PHHY is proposed. By PHHY, it is proved that there is a universally efficient algorithm for solving SAT problem. Then, by square packing problem, the authors sh... From the SAT physical model, a physical hypothesis named PHHY is proposed. By PHHY, it is proved that there is a universally efficient algorithm for solving SAT problem. Then, by square packing problem, the authors show that there are interesting industrial NP-complete problems which can be solved through SAT algorithms, but each way of solving like this will be much worse than that of a certain direct solving. 展开更多
关键词 NP-complete problem CNF-sat satisfiability potential function approximate algorithm PROBABILITY complexity.
原文传递
PSL的有界模型检验 被引量:2
6
作者 虞蕾 赵宗涛 《电子学报》 EI CAS CSCD 北大核心 2009年第3期614-621,共8页
基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性... 基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程. 展开更多
关键词 PSL(property specification language) 有界模型检验(bounded model checking BMC) sat(propositional satisfiability) OBDD(ordered binary decision diagram)
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部