SLS算法求解平衡正则（k,2r）-CNF公式

发布时间：2021-07-22 23:28

　　可满足性问题的求解算法和结构性质研究是计算机科学中重要问题之一,为寻求某些CNF公式子类问题有效算法或算法改进途径,对公式的结构加以某些限制,其中限定子句长度为恒定常数和变元出现次数是常见的处理方式。研究具有正则结构且每个变元正负出现均衡的结构化公式的可满足性问题求解,其随机生成模型的构建及随机实验测试有助于观察解分布状况。并且,随机局部搜索算法在求解具有一定规则结构CNF公式实例中具有良好效率。本文集中研究平衡正则（k,2r）-CNF公式的求解问题,即限制每个子句的长度为k,每个变元出现的次数为偶数2r,并且每个变元正负出现的次数在相等情况下的可满足性问题求解。给出BR（n,k,2r）模型,以此模型来生成具有特殊结构的平衡正则（k,2r）-CNF公式实例,利用随机局部搜索算法求解问题。通过限制初始指派的0文字和1文字各占一半且均匀生成,以Walk SAT算法和NSAT算法做实验对比,发现对于平衡正则（k,2r）-CNF公式,实例具有明显效率。 

【文章来源】：计算机与现代化. 2019,(01)

【文章页数】：5 页

【部分图文】：

初始指派被限制的实例类ＲegFormula-5000-3-8在SLS算法下的求解时间

【参考文献】：
期刊论文
[1]基于人工智能路径规划系统的智能小车的设计与实现[J]. 蔡莉莎,曾维鹏.  电子世界. 2016(18)
[2]基于加强概率控制策略的SAT局部搜索算法[J]. 洪剑珂,张峥华,许贵平.  计算机工程与应用. 2017(14)
[3]正则3-SAT问题的相变现象[J]. 张明明,许道云.  计算机科学. 2016(04)
[4]极小不可满足公式在多项式归约中的应用[J]. 许道云.  软件学报. 2006(05)
[5]SAT问题中局部搜索法的改进[J]. 杨晋吉,苏开乐.  计算机研究与发展. 2005(01)
[6]AI规划的回顾与展望[J]. 刘吉颖,方思行.  中山大学学报论丛. 2000(05)
[7]求解SAT问题的局部搜索算法及其平均时间复杂性分析[J]. 刘涛,李国杰.  计算机学报. 1997(01)

博士论文
[1]自动推理与规划问题最小上界和相变规律研究[D]. 周俊萍.吉林大学 2011

硕士论文
[1]基于FPGA镆拟的SAT求解方法[D]. 毛乐乐.广西民族大学 2016
[2]基于SAT的数字电路ATPG方法及应用[D]. 张岳华.吉林大学 2012
[3]基于SAT的VLSI测试向量自动生成技术[D]. 付宇.北京交通大学 2010



本文编号：3298116