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公式,实例具有明显效率。

SLS Algorithm for Solving Equilibrium Regular(k,2r)-CNF Formula

The research on solving algorithms and structural properties of satisfiability problems is one of the important issues in computer science. In order to find some effective methods or algorithm improvement methods for some subclass problems of CNF formula, some restrictions are imposed on the structure of the formula. It is a common treatment to limit the length of a clause to a constant and the number of occurrences of arguments. The problem of satisfiability of structured formulas with regular structure and equalization of positive and negative occurrences per argument is studied. The construction of stochastic generation models and random experimental tests are helpful to observe the distribution of solutions. Moreover, the stochastic local search algorithm has good efficiency in solving the instance of a CNF formula with a certain regular structure. This paper focuses on the solution of the equilibrium regular (k, 2r)-CNF formula, that is, to solve the satisfiability problem under the condition that the length of each clause is limited to k, and the number of occurrences of each argument is exactly 2r, and the number of positive and negative occurrences of each argument is equal. The BR(n, k, 2r) model is given, this model is used to generate an equilibrium regular (k, 2r)-CNF formula with special structure, and the problem is solved by a stochastic local search algorithm. By limiting the initial assignment of 0 word and 1 word to half and uniformly generating, the comparison between WalkSAT algorithm and NSAT algorithm shows that the instance of equilibrium regular (k, 2r)-CNF formula has obvious efficiency.