论文摘要
可满足性问题（Boolean Satisfiability Problem,简称SAT）是一个关于判断一个布尔表达式是否可为真的问题。而布尔表达式都可以转换成或与表达式（Conjurictive Normal Form,简称CNF）。本文介绍的是作者在SAT问题算法方面的一些研究,以及对于通过简化CNF来提高解决SAT问题的效率的策略。在实际应用中,可满足性问题有许多应用,例如在电子设计自动化（Electronic Design Automation,简称EDA）中,形式验证（FormalVerification）验证逻辑电路等效性就常将可满足性算法作为引擎。由于逻辑电路的复杂度高,且重复性也比较高,本文尝试利用布尔表达式的蕴含和化简公式来简化CNF的方法以提高SAT解决器的效率。程序用C++及STL标准模板库编程实现,将原始的CNF式转化成简化后的CNF,再使用zchaff解决新的CNF式来提高SAT解决器的效率。实验结果显示简化程序成功地简化了CNF式,简化及Zchaff解决新CNF式的总时间消耗小于使用Zchaff直接解决原CNF的时间。
论文目录
相关论文文献
- [1].红外光激励的CNF复合微悬臂梁稳态响应特性[J]. 湖南城市学院学报(自然科学版) 2017(02)
- [2].接枝改性CNF增强聚丙烯酸酯复合膜制备及性能[J]. 工程塑料应用 2020(10)
- [3].基于自适应模糊补偿的不确定性机器人CNF控制[J]. 振动与冲击 2020(08)
- [4].用作气相催化反应体系CNF/泡沫炭催化剂载体的合成(英文)[J]. 新型炭材料 2011(05)
- [5].CNF控制算法在大型客机自动着陆中的应用[J]. 系统仿真学报 2012(12)
- [6].表面改性CNF对PBS/PLA共混物的湿热老化行为的影响[J]. 中国塑料 2019(12)
- [7].炭黑/CNF复合光热转化材料的制备及性能研究[J]. 中国造纸 2020(07)
- [8].等离子体处理对PLA膜亲水性及与CNF膜粘附性的影响[J]. 包装工程 2020(15)
- [9].大黄提取物对兔耳静脉炎组织中CNF-κB表达的影响[J]. 浙江中医杂志 2014(04)
- [10].PUR-T协同CNF对PLA结晶及力学性能的影响[J]. 工程塑料应用 2019(11)
- [11].四旋翼无人机高度控制——基于CNF与自适应非光滑控制[J]. 福建工程学院学报 2018(01)
- [12].氨基化球形CNF气凝胶的制备及其性能[J]. 材料科学与工程学报 2019(05)
- [13].不同CNF添加量对CNC气凝胶结构与性能的影响[J]. 东北林业大学学报 2018(08)
- [14].植物纤维基电气绝缘纸的强度性能[J]. 天津科技大学学报 2020(01)
- [15].CNF公式赋值空间上可满足解的概率性质[J]. 计算机科学与探索 2018(11)
- [16].基于因子图求解(3,4=)-CNF公式类下可满足问题[J]. 计算机与数字工程 2013(05)
- [17].SLS算法求解平衡正则(k,2r)-CNF公式[J]. 计算机与现代化 2019(01)
- [18].日本纸和纸板的生产、消费及研究开发进展——2015年、2016年供需状况和CNF事业进展[J]. 中国造纸 2016(09)
- [19].结合AIG和两变量观测策略的SAT满足性算法[J]. 电路与系统学报 2013(01)
- [20].2-CNF理论的逻辑差[J]. 计算机应用研究 2015(09)
- [21].基于CNF权重学习求解3-SAT问题的进化算法[J]. 贵州大学学报(自然科学版) 2009(05)