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

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

正则3-SAT问题的相变现象

通过对3-CNF公式加以限制,要求其中每个变元出现的次数相同,引出正则3-SAT问题。进一步,通过对两种子句产生机制形成的(3,s)-CNF公式进行可满足性观察,发现在规模较小的情况下,正则3-CNF公式比非正则3-CNF公式更容易满足。从而推测与非正则3-SAT问题相比,正则3-SAT问题的相变点有偏移现象。最后,从变元自由度的角度对这一现象给出了定性解释。