检索结果-南通市图书馆

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

可满足模理论在软硬件划分领域的应用

广西民族大学学报（自然科学版） 2016年第1期22卷 78-82页

作者：毛乐乐胡小勤卢晨广西民族大学广西混杂计算与集成电路设计分析重点实验室广西南宁530006 广西民族大学信息科学与工程学院广西南宁530006

软硬件划分是评价软硬件协同设计优劣,甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题,借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案,使得系统的软硬件实现代价最小,经实验验证,针对... 详细信息

软硬件划分是评价软硬件协同设计优劣,甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题,借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案,使得系统的软硬件实现代价最小,经实验验证,针对软硬件划分问题,Z3的综合性能要优于另外两种解决器.采用可满足性问题求解方案,不仅克服了传统启发式算法陷入局部最优解的弊端,同时也弥补了规划类算法不适应于大规模划分问题的不足.

关键词：软硬件协同设计软硬件划分可满足模理论可满足模理论求解器

在线全文

学校读者我要写书评

暂无评论

一种可满足模理论的拟物优化求解算法

福建电脑 2021年第7期37卷 23-26页

作者：卢道设广州华夏职业学院信息工程学院广州510935

为了研究改善可满足性模理论的求解效率,本文基于拟物方法结合萤火虫优化算法,设计出新的优化求解方案。实验结果表明,使用萤火虫优化算法求解可满足性问题在特定应用案例上效果显著,基于Benchmarks(可满足模理论求解器公开基准测试案例... 详细信息

为了研究改善可满足性模理论的求解效率,本文基于拟物方法结合萤火虫优化算法,设计出新的优化求解方案。实验结果表明,使用萤火虫优化算法求解可满足性问题在特定应用案例上效果显著,基于Benchmarks(可满足模理论求解器公开基准测试案例库)的基准测试案例中求解效率平均比纯拟物拟人算法上提高至少10%的性能。基于拟物方法结合最优化算法在特定领域的可满足性求解算法不仅容易实现,同时能有效提高求解效率。

关键词：拟物拟人算法可满足模理论萤火虫优化算法 SAT 最优化算法

在线全文

学校读者我要写书评

暂无评论

SMT求解器理论组合技术研究

计算机工程与科学 2011年第10期33卷 111-119页

作者：李婧刘万伟并行与分布处理国防科技重点实验室湖南长沙410073

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述... 详细信息

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。

关键词：可满足模理论 SMT求解器组合理论

在线全文

学校读者我要写书评

暂无评论

不可满足子式研究

智能系统学报 2013年第6期8卷 497-504页

作者：殷明浩李欣东北师范大学计算机科学与信息技术学院吉林长春130117

为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域,对不可满足子式进行了相关研究.对当前不可满足子式的主要相关算法进行了概述评论、分类归纳,并从计算复杂性角度介绍了其子类、参数复杂性以及QB... 详细信息

为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域,对不可满足子式进行了相关研究.对当前不可满足子式的主要相关算法进行了概述评论、分类归纳,并从计算复杂性角度介绍了其子类、参数复杂性以及QBF中的极小不可满足子式.总结了近10年来不可满足子式的理论与算法,讨论了不可满足子式的未来研究发展方向.研究有利于进一步发现不可满足的根本原因,从而进行有针对性地改进,并对相关人员的研究提供帮助.

关键词：可满足性问题不可满足子式可满足模理论局部搜索

在线全文

学校读者我要写书评

暂无评论

FPGA板级路由问题的SMT方法研究

FPGA板级路由问题的SMT方法研究

作者：吴昊广西民族大学

学位级别：硕士

FPGA板级路由问题是电路设计环节中的一个重要问题,它主要解决的问题是当把一个大规模电路设计划分成多个模块,并把多个模块封装到多个FPGA芯片中之后,如何用多个多端网把每个FPGA芯片按特定要求链接起来,实现信息路由通常的问题。而面... 详细信息

FPGA板级路由问题是电路设计环节中的一个重要问题,它主要解决的问题是当把一个大规模电路设计划分成多个模块,并把多个模块封装到多个FPGA芯片中之后,如何用多个多端网把每个FPGA芯片按特定要求链接起来,实现信息路由通常的问题。而面对集成电路规模的增长,使得问题规模越来越大,如何高效解决FPGA板级路由问题是该领域的一个研究热点。本文通过对该问题的研究,提出了一种基于可满足模理论(Satisfiability Modulo Theories,简称SMT)的方法来解决该问题。经过对该问题和SMT的深入研究,本文主要取得了以下成果：建立了FPGA板级路由问题的算术模型,并转化成SMT表达式,最后用SMT解决器求解;提出了一种约化该问题的方法,通过约减多端网的数量,以到达缩减问题规模的目的,并用SMT方法求解。实验表明,采用SMT方法具有更高的解决问题效率,具备处理更大规模问题的能力;此外约减方法对基于SMT方法的计算效率有一定的提高。

关键词： FPGA 板级路由问题集成电路设计可满足模理论理论解决器