Abstract: 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.

Key words: SAT problem, regular CNF formula, stochastic local search, WalkSAT algorithm, NSAT algorithm