布尔可满足性

作品数:42被引量:43H指数:3
导出分析报告
相关领域:电子电信自动化与计算机技术更多>>
相关作者:刘歆李光辉邵明李晓维黎铁军更多>>
相关机构:浙江大学国防科学技术大学湖北工业大学浙江林学院更多>>
相关期刊:《清华大学学报(自然科学版)》《电子科技文摘》《计算机工程与应用》《交通科技与经济》更多>>
相关基金:国家自然科学基金浙江省自然科学基金国家高技术研究发展计划国家重点基础研究发展计划更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
基于布尔可满足性的精确逻辑综合综述被引量:2
《电子与信息学报》2023年第1期14-23,共10页储著飞 潘鸿洋 
国家自然科学基金(61871242);专用集成电路与系统国家重点实验室开放研究课题基金(2021KF008)。
逻辑综合是电子设计自动化(EDA)的重要步骤,随着算力逐渐提升和新的计算范式不断涌现,传统基于全局启发式算法的逻辑综合面临新的挑战。启发式算法面临的主要问题是得到一个次优解,随着算力的提升,逻辑优化越来越追求精确解而不满足于...
关键词:逻辑综合 精确综合 布尔可满足性 多数逻辑门 
基于消息传递关系网络的布尔可满足性预测被引量:1
《软件学报》2022年第8期2839-2850,共12页包冬庆 葛宁 翟树茂 张莉 
国家自然科学基金(61902011,61690202);北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
布尔可满足性求解能够验证的问题规模通常受限,因此,如何高精度地预测其可满足性既是重要的研究问题,也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构,但是这种表征方法缺少...
关键词:布尔可满足性问题 消息传递网络 结构特征 可满足性预测 多关系异构图 
一种加速FPGA布线的不可满足子式求解算法
《电子学报》2021年第6期1210-1216,共7页张建民 黎铁军 马柯帆 肖立权 
国家自然科学基金(No.62072464,No.U19A2062);并行与分布处理国家级重点实验室开放基金(No.WDZC20205500116)。
随着VLSI(Very Large Scale Integrated)芯片设计的规模越来越大,功能越来越复杂,在FPGA(Field Programmable Gate Array)上实现或进行原型验证时,往往会出现布线拥塞或无法布通的情况.而不可满足子式能够迅速诊断FPGA无法布通的原因,...
关键词:FPGA布线 布线约束 布尔可满足性 不可满足子式 局部搜索 消解否证 
基于SAT的分离制造攻击方法
《复旦学报(自然科学版)》2019年第6期696-705,718,共11页刘佳琳 陆昆 严昌浩 周海 周电 曾璇 
芯片代工厂可能进行诸如IP盗版、过度生产和硬件木马插入等一系列的恶意攻击.分离制造是一种抵御来自芯片代工厂芯片攻击的重要技术.针对分离制造工艺,目前最好的攻击方法是基于网络流的邻近攻击算法,但在多数情况下,这种邻近攻击算法...
关键词:分离制造 布尔可满足性 CycSAT 基于SAT的攻击 
加强约束的布尔可满足硬件求解器被引量:1
《国防科技大学学报》2018年第6期105-111,共7页马柯帆 肖立权 张建民 黎铁军 周善祥 
国家自然科学基金资助项目(61103083;61133007;61572509);国家重点基础研究发展计划资助项目(2016YFB0200203)
利用现场可编程门阵列固有的并行性和灵活性,提出在硬件可编程平台上基于随机局部搜索算法的布尔可满足性求解器,用于求解大规模的布尔可满足性问题。相对其他求解器,该求解器的预处理技术能极大提高求解效率;其变元加强策略避免了同一...
关键词:现场可编程门阵列 布尔可满足性 加强约束 不完全算法 
基于SAT和BDD的频繁序列挖掘技术被引量:1
《广西科学院学报》2018年第2期137-142,150,共7页戴瑀君 徐周波 
广西自然科学基金项目(2017GXNSFAA198172)资助
【目的】研究模式挖掘领域中的频繁序列挖掘技术,由于序列模式挖掘存在指数级的搜索空间,且传统的SAT求解算法无法高效求解大规模数据集的缺点,因此研究符号表示和操作技术,用来避免冗余计算。【方法】提出基于SAT的频繁序列挖掘的符号O...
关键词:布尔可满足性 有序二叉决策图 频繁序列挖掘 
串扰时延故障的SAT-ATPG算法研究
《计算机测量与控制》2017年第3期18-21,共4页尚玉玲 钱尚 刘鹏 
随着芯片运行速度不断提高,对串扰时延的测试已成为一个迫切需要解决的问题;文中提出一种面向多条攻击线的受害线上最大串扰噪声的测试生成方法;此方法建立了串扰通路时延故障模型、分析了布尔可满足性问题、讨论了七值逻辑,研究了串扰...
关键词:串扰时延故障 布尔可满足性 时延测试 
基于聚类和划分的SAT分治判定被引量:1
《软件学报》2015年第9期2155-2166,共12页范全润 段振华 
国家自然科学基金(61133001;61322202;61420106004)
提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂...
关键词:合取范式 布尔可满足性 划分 聚类 
基于SAT的安全协议惰性形式化分析方法被引量:2
《通信学报》2014年第11期117-125,共9页顾纯祥 王焕孝 郑永辉 辛丹 刘楠 
河南省科技创新杰出青年基金资助项目(134100510002);河南省基础与前沿技术研究基金资助项目(142300410002);数学工程与先进计算国家重点实验室开放基金资助项目~~
提出了一种基于布尔可满足性问题的安全协议形式化分析方法 SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此...
关键词:安全协议 形式化分析 布尔可满足性 惰性分析 类型缺陷攻击 
时序电路等价验证的触发器匹配被引量:1
《电子与信息学报》2014年第9期2283-2286,共4页张超 竺红卫 
通常的时序电路等价性验证方法是将触发器按时序展开,从而将时序电路转化为组合电路进行验证。而一般在待验证的两个时序电路中,触发器是一一对应的,找到触发器的对应关系,时序电路的验证就会得到很大的简化。该文通过一种新的基于布尔...
关键词:触发器匹配 自动测试模式生成模型 布尔可满足性 时序帧递进展开 信息学习 
检索报告 对象比较 聚类工具 使用帮助 返回顶部