检索结果-南通市图书馆

基于悖论证明与局部搜索的不可满足子式求解算法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2014年第11期37卷 2262-2267页

作者：张建民沈胜宇李思昆国防科学技术大学计算机学院长沙410073

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法... 详细信息

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.

关键词：形式化验证可满足问题不可满足子式悖论证明局部搜索

在线全文

学校读者我要写书评

暂无评论

基于局部搜索的并行扩展规则推理方法

软件学报 2021年第9期32卷 2744-2754页

作者：李壮刘磊张桐搏周文博吕帅吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 吉林长春130012

扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可,例如完备的NER,IMOMH_IER,PPSER算法以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算... 详细信息

扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可,例如完备的NER,IMOMH_IER,PPSER算法以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算法是当前扩展规则求解器中求解效率最高、能力最强的算法.但是,串行的ERACC算法在启发式和预处理上仍然具有可提升的空间.基于此,设计了相应的并行框架,提出了PERACC算法.该算法基于格局检测的局部搜索方法,从变量赋初始值、化简解空间和启发式这3个阶段出发,将原极大项空间分解成为若干极大项子空间,并对原子句集进行化简后,并行处理各个子空间.通过实验显示:该算法与原算法相比,不仅在求解效率方面有较大提高,而且可以求解规模更大的测试用例,使扩展规则方法再次突破公式规模的限制.

关键词：自动推理局部搜索扩展规则格局检测并行框架

在线全文

学校读者我要写书评

暂无评论

SAT问题中局部搜索法的改进

计算机研究与发展 2005年第1期42卷 60-65页

作者：杨晋吉苏开乐中山大学信息科学与技术学院计算机科学系华南师范大学计算机科学系广州 510631 河南科技大学电子信息工程学院洛阳 471003

局部搜索方法在求解SAT问题的高效率使其成为一研究热点.提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束.使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度.用该方法对目前... 详细信息

局部搜索方法在求解SAT问题的高效率使其成为一研究热点.提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束.使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度.用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高.该方法对其他局部搜索法的改进具有参考价值。

关键词： SAT问题局部搜索概率

在线全文

学校读者我要写书评

暂无评论

基于局部搜索的反向学习竞争粒子群优化算法

控制与决策 2021年第4期36卷 779-789页

作者：钱晓宇方伟江南大学物联网工程学院江苏无锡214122

为提升粒子群优化算法在复杂优化问题,特别是高维优化问题上的优化性能,提出一种基于Solis&Wets局部搜索的反向学习竞争粒子群优化算法(solis and wets-opposition based learning competitive particle swarm optimizer with local search, SW-OBLCSO). SW-OBLCSO算法采用竞争学习和反向学习两种学习机制,并设计了基于个体的局部搜索算子.利用10个常用基准测试函数和12个带有偏移旋转的复杂测试函数,在不同维度情况下将SW-OBLCSO算法与多种优化算法进行对比.实验结果表明,所提出算法在收敛速度和全局搜索能力上表现出突出的性能.对模糊认知图(fuzzy cognitive maps)学习问题的测试表明, SW-OBLCSO算法在处理实际问题时同样具有出色的性能.

关键词：粒子群优化算法反向学习大规模优化问题竞争学习局部搜索高维优化

在线全文

学校读者我要写书评

暂无评论

一种基于区域局部搜索的NSGA Ⅱ算法

自动化学报 2020年第12期46卷 2617-2627页

作者：栗三一王延峰乔俊飞黄金花郑州轻工业学院郑州450002 北京工业大学信息学部北京100124 武汉船舶职业技术学院武汉430000

针对局部搜索类非支配排序遗传算法(Nondominated sorting genetic algorithms, NSGA Ⅱ)计算量大的问题,提出一种基于区域局部搜索的NSGA Ⅱ算法(NSGA Ⅱ based on regional local search, NSGA Ⅱ-RLS).首先对当前所有种群进行非支配... 详细信息

针对局部搜索类非支配排序遗传算法(Nondominated sorting genetic algorithms, NSGA Ⅱ)计算量大的问题,提出一种基于区域局部搜索的NSGA Ⅱ算法(NSGA Ⅱ based on regional local search, NSGA Ⅱ-RLS).首先对当前所有种群进行非支配排序,根据排序结果获得交界点和稀疏点,将其定义为交界区域和稀疏区域中心;其次,围绕交界点和稀疏点进行局部搜索.在局部搜索过程中,同时采用极限优化策略和随机搜索策略以提高解的质量和收敛速度,并设计自适应参数动态调节局部搜索范围.通过ZDT和DTLZ系列基准函数对NSGA Ⅱ-RLS算法进行验证,并将结果与其他局部搜索类算法进行对比,实验结果表明NSGA Ⅱ-RLS算法在较短时间内收敛速度和解的质量方面均优于所对比算法.

关键词：非支配排序遗传算法分区搜索局部搜索多目标优化

在线全文

学校读者我要写书评

暂无评论

一种新的基于局部搜索的扩展规则推理方法

计算机学报 2018年第4期41卷 825-839页

作者：杨洋刘磊李广力张桐搏吕帅吉林大学计算机科学与技术学院长春130012 吉林大学数学学院长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 长春130012

作为与归结推理方法互补的推理方法,扩展规则推理方法得到了国内外广泛认可.目前扩展规则推理方法的研究主要集中于完备推理方法,由于极大项变换方式过于机械,导致该方法处理公式的规模比较局限.该文在深入分析扩展规则推理和局部搜索... 详细信息

作为与归结推理方法互补的推理方法,扩展规则推理方法得到了国内外广泛认可.目前扩展规则推理方法的研究主要集中于完备推理方法,由于极大项变换方式过于机械,导致该方法处理公式的规模比较局限.该文在深入分析扩展规则推理和局部搜索关联性的基础上,利用子句集中的"极大项"概念设计了一种反向求解策略,进而设计并实现一种新的基于局部搜索的扩展规则推理框架.在此基础上,为了使得极大项搜索过程更加适配该框架,提出了一种基于精确格局检测实现和双向半扩展规则策略的两阶段局部搜索算法.实验结果表明,该文提出的基于精确格局检测的新型扩展规则推理算法ERACC突破了传统扩展规则推理对公式规模的局限,求解效率有了极大提高,使得扩展规则推理方法不再受公式规模制约,可以用于知识编译和可能性推理等多方面的应用.

关键词：自动推理扩展规则局部搜索精确格局检测双向半扩展规则反向求解

在线全文

学校读者我要写书评

暂无评论

基于局部搜索OMP的网格失配STAP算法

系统工程与电子技术 2018年第6期40卷 1221-1226页

作者：李志汇张永顺高乾郭艺夺王强刘洋空军工程大学防空反导学院陕西西安710051 信息感知技术协同创新中心陕西西安710077 空军通信士官学校辽宁大连116600

针对稀疏恢复空时自适应处理(space-time adaptive processing,STAP)存在网格失配时,造成稀疏恢复STAP的性能下降这一问题,提出一种基于局部搜索正交匹配追踪算法。该算法首先从全局STAP完备字典中选择与杂波相匹配的全局网格点;然后以... 详细信息

针对稀疏恢复空时自适应处理(space-time adaptive processing,STAP)存在网格失配时,造成稀疏恢复STAP的性能下降这一问题,提出一种基于局部搜索正交匹配追踪算法。该算法首先从全局STAP完备字典中选择与杂波相匹配的全局网格点;然后以选出的全局网格点为中心,以全局完备STAP字典的空时频率间隔为区域,构建局部STAP字典,并从中选择与杂波最匹配的局部网格点;最后得到杂波的角度-多普勒像和修正的STAP字典。仿真结果表明,所提的算法能够选择与真实杂波脊相匹配的网格点,从而提高了稀疏恢复STAP技术的性能。

关键词：空时自适应处理稀疏恢复网格失配局部搜索正交匹配追踪

k-Median近似计算复杂度与局部搜索近似算法分析

在线全文

学校读者我要写书评

暂无评论

软件学报 2005年第3期16卷 392-399页

作者：潘锐朱大铭马绍汉肖进杰山东大学计算机科学与技术学院山东济南250061 山东工商学院信息与电子工程学院山东烟台264005

k-Median 问题的近似算法研究一直是计算机科学工作者关注的焦点,现有研究结果大多是关于欧式空间和 Metric 空间的,一般距离空间 k-Median 的结果多年来一直未见.考虑一般距离空间 k-Median 问题,设 dmax/dmin表示 k-Median 实例中与... 详细信息

k-Median 问题的近似算法研究一直是计算机科学工作者关注的焦点,现有研究结果大多是关于欧式空间和 Metric 空间的,一般距离空间 k-Median 的结果多年来一直未见.考虑一般距离空间 k-Median 问题,设 dmax/dmin表示 k-Median 实例中与客户点邻接的最长边长比最短边长的最大者.首先证明 dmax/dmin≤ω+ε的 k-Median 问题不存在近似度小于1+ ω ?1 (loglog n) e 的多项式时间近似算法,除非 NP ? DTIME(nO ) ,由此推出 Metric k-Median 问题不可近似到 1+ 2 (log log n) e,除非 NP ? DTIME(nO ) .然后给出 k-Median 问题的一个局部搜索算法,分析表明,若有 dmax/dmin≤ω,则算法的近似度为 1+ ω2 .该结果亦适用于 Metric k-Median,ω≤5 时,局部搜索算法求解 Metric k-Median 的 ?1近似度为 3,好于现有结果 3+ 2 .通过计算机实验,进一步研究了 k-Median 局部搜索求解算法的实际计算效果和该 p算法的改进方法.

关键词： κ中间点算法局部搜索近似度设备客户

在线全文

学校读者我要写书评

暂无评论

基于IAPS的扩展规则局部搜索算法

电子学报 2020年第5期48卷 899-905页

作者：王金艳胡春牛当当李先贤广西多源信息挖掘与安全重点实验室(广西师范大学) 广西桂林541004 广西师范大学计算机科学与信息工程学院广西桂林541004 西北农林科技大学信息工程学院陕西杨凌712100

ERACC(Extension Rule Based on Accurate Configuration Checking)算法由杨洋等人基于扩展规则和格局检测提出,具有较高的推理效率.为进一步提高ERACC算法在大规模SAT(Satisfiability)问题求解上的性能,本文在搜索由极大项组成的空间时... 详细信息

ERACC(Extension Rule Based on Accurate Configuration Checking)算法由杨洋等人基于扩展规则和格局检测提出,具有较高的推理效率.为进一步提高ERACC算法在大规模SAT(Satisfiability)问题求解上的性能,本文在搜索由极大项组成的空间时,首先利用IMOM(Improved Maximum Occurrences on Clauses of Maximum Size)思想生成初始极大项,接着设计了适用于扩展规则推理的CCA_ER(Configuration Checking with Aspiration for Extension Rule-Based Reasoning)启发式策略,为极大项中格局信息未发生变化的变量对应文字提供一定的翻转机会.同时,为进一步提高扩展规则推理算法在k-SAT问题求解上的性能,设计了适用于扩展规则推理的PAWS_ER(Pure Additive Weighting Scheme for Extension Rule-Based Reasoning)策略,并且给出变量的Subscore_ER(Subscore for Extension Rule-Based Reasoning),CScore_ER(Comprehensive Score for Extension Rule-Based Reasoning)和HScore_ER(Hybrid Score for Extension Rule-Based Reasoning)属性.在此基础上,提出了ERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER and Subscore_ER)和CERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER,CScore_ER and HScore_ER)算法.实验结果表明:ERACC_IAPS和CERACC_IAPS算法的效率明显优于ERACC算法,最高可将其求解效率提高1000多倍.

关键词：扩展规则自动推理局部搜索格局检测