共查询到10条相似文献,搜索用时 15 毫秒
1.
由一阶逻辑公式得到命题逻辑可满足性问题实例 总被引:2,自引:0,他引:2
命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题. 相似文献
2.
在纳米尺度的集成电路设计中,冗余通孔插入是减轻通孔失效造成良率降低问题的常用技术.文中将最优冗余通孔插入问题规约到命题逻辑最大逻辑可满足性(maximum satisfiability, Max SAT)问题,并利用完备求解器求取最优解.MaxSAT问题是一个NP困难问题,采用2种方法来降低求解难度;一是预选取方法,将提前确定的不与其他通孔产生冲突的冗余通孔作为部分解来降低问题的规模;二是分治法,根据连通分量将原问题划分成多个子问题分别求解,降低求解的复杂度.同时,从理论上证明这2种方法能够保证解的最优性.在2019年国际物理设计研讨会(ISPD)举办的详细布线比赛基准测试集上进行实验的结果表明,所提出的插入方法带来的时间开销不到详细布线时间的5%,算法的最优性保证了最大化解决插入冲突后的插入率,在所有可插入通孔中,冗余通孔的插入率为67%~87%. 相似文献
3.
该文为可满足性问题的高效近似求解提出了改进的模拟退火算法。数值实验表明,对于该文随机产生的测试问题例,改进的模拟退火算法完全胜过局部搜索算法、模拟退火算法以及目前国际上流行的WSAT算法。 相似文献
4.
求解难可满足性问题的混合算法 总被引:1,自引:0,他引:1
张德富 《小型微型计算机系统》2003,24(8):1528-1531
提出了一个求解难可满足性问题的简单混合算法.拟人和禁忌表两个策略被给出.数值实验表明,对于一类公认比较难的可满足性问题,该算法胜过目前据认为是最好方法之一的NOVELTY算法. 相似文献
5.
约束可满足性问题是一大类常出现于现实应用中的复杂问题,因其繁多的约束条件而出名。本文针对一个经典的约束可满足性问题——斑马属谁问题.基于演化算法的框架进行求解。我们采用矩阵的表示方式.并设计了相应的杂交和变异算予。实验表明.演化算法能高效地解决该问题。 相似文献
6.
7.
8.
对SAT问题及其各种约束子问题进行分类并给出具体定义,着重介绍常规SAT问题、最大可满足性问题(MAX—SAT)和参数化SAT问题的相关算法,并对参数算法中运用的技术进行分析和比较,提出一些SAT问题研究中值得关注的几个方面。 相似文献
9.
SAT问题在人工智能、计算机基础理论研究和人工智能等领域有着广泛的应用,近年来,证明该问题的可满足性取得了巨大的成功,但在求出SAT问题的所有解方面还有待进一步研究。利用一个简单的变换,将可满足性(SAT)问题转化为多项式形式,然后根据命题逻辑的性质以及多项式的性质,得到一个求解出SAT问题所有解的算法。实验结果显示该算法是有效和可行的。 相似文献