求解#SMT问题的局部搜索算法

发布时间：2017-11-02 18:38

  本文关键词：求解#SMT问题的局部搜索算法

  更多相关文章： #SMT 满足性 差分进化 线性公式

【摘要】：#SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——Vol Compute With Local Search.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了Vol Compute With Local Search求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明:Vol Compute With Local Search求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.
【作者单位】： 东北师范大学计算机科学与信息技术学院;
【关键词】： #SMT 满足性 差分进化 线性公式
【基金】：国家自然科学基金(61370156,61403076,61403077) 高等学校博士学科点专项科研基金(20120043120017) 新世纪优秀人才支持计划(NCET-13-0724) 吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03)~~
【分类号】：TP18
【正文快照】： 命题可满足性问题(简称SAT问题)是计算机科学领域的重要研究问题之一,作为第一个被证明为NP完全的问题[1],许多实际问题如电路设计、自动定理证明、限界模型检验、等价性检查都可以在多项式时间内转为SAT问题进行求解.但由于SAT问题以命题逻辑公式为处理对象,制约了其描述能力

【相似文献】

中国期刊全文数据库 前10条

1 吴燕玲;卢建刚;孙优贤;;基于免疫原理的差分进化[J];控制与决策;2007年11期

2 杨启文;蔡亮;薛云灿;;差分进化算法综述[J];模式识别与人工智能;2008年04期

3 许小健;黄小平;钱德玲;;自适应加速差分进化算法[J];复杂系统与复杂性科学;2008年01期

4 宁桂英;周永权;;基于优进策略的新差分进化算法动力学模型参数的估计[J];计算机与应用化学;2008年05期

5 谭跃;谭冠政;涂立;;一种新的混沌差分进化算法[J];计算机工程;2009年11期

6 王培崇;钱旭;王月;虎晓红;;差分进化计算研究综述[J];计算机工程与应用;2009年28期

7 肖术骏;朱学峰;;一种改进的快速高效的差分进化算法[J];合肥工业大学学报(自然科学版);2009年11期

8 周萧;王万良;徐新黎;;解决作业车间调度问题的混合差分进化算法[J];轻工机械;2010年05期

9 王艳宜;;改进差分进化算法及其应用[J];机械设计与研究;2010年05期

10 张照生;罗健旭;;基于差分进化算法的模糊神经网络控制器[J];计算机与应用化学;2011年12期

中国重要会议论文全文数据库 前5条

1 陆丝馨;肖健梅;王锡淮;;基于改进差分进化算法的舰船电网重构[A];第二十九届中国控制会议论文集[C];2010年

2 张倩;李海港;;多目标问题的差分进化算法研究[A];2009年中国智能自动化会议论文集（第一分册）[C];2009年

3 刘国帅;杨侃;陈静;周景舒;周冉;郑姣;;差分进化算法在三峡电站厂内经济运行中的应用[A];中国水文科技新发展——2012中国水文学术讨论会论文集[C];2012年

4 倪惠康;杜文莉;钱锋;;基于改进差分进化算法的PID参数优[A];2009年中国智能自动化会议论文集（第一分册）[C];2009年

5 雍龙泉;;求解一类多目标优化问题的极大熵差分进化算法[A];2013年中国智能自动化学术会议论文集（第五分册）[C];2013年

中国博士学位论文全文数据库 前10条

1 孙浩;差分进化多目标优化算法及其在铝热连轧轧制规程中应用[D];燕山大学;2015年

2 谢宇;差分进化的若干问题及其应用研究[D];南京理工大学;2015年

3 刘荣辉;多阶段自适应差分进化算法及应用研究[D];东华大学;2012年

4 王旭;改进差分进化算法及其在可逆逻辑综合中的应用[D];东华大学;2013年

5 董明刚;基于差分进化的优化算法及应用研究[D];浙江大学;2012年

6 丁青锋;基于元胞自动机的差分进化算法及其在通信系统中的应用研究[D];上海大学;2015年

7 徐斌;基于差分进化算法的多目标优化方法研究及其应用[D];华东理工大学;2013年

8 解为成;基于局部摸索的差分进化算法及其在曲面重建中的应用[D];武汉大学;2013年

9 孙成富;差分进化算法及其在电力系统调度优化中的应用研究[D];华中科技大学;2010年

10 向万里;混合群体智能优化算法及应用研究[D];天津大学;2014年

中国硕士学位论文全文数据库 前10条

1 万婧;基于离散微粒群算法和混合差分进化算法的复杂生产调度问题求解[D];昆明理工大学;2015年

2 程菲;膜计算在数值优化问题中的应用研究[D];西华大学;2015年

3 袁文龙;基于控制思想的差分进化算法改进研究[D];东北大学;2014年

4 刘文壮;基于差分进化的约束求解算法研究[D];吉林大学;2016年

5 唐亚;差分进化算法的改进及其在聚类中的应用[D];广东工业大学;2016年

6 张转;基于差分进化算法的混凝土德拜模型的研究[D];长安大学;2015年

7 宁桂英;差分进化算法及其应用研究[D];广西民族大学;2008年

8 刘俊梅;混合差分进化算法及应用研究[D];北方民族大学;2010年

9 王洪波;基于差分进化计算的聚类算法研究[D];山东师范大学;2012年

10 呼忠权;差分进化算法的优化及其应用研究[D];燕山大学;2013年

，

本文编号：1132702