关键词: 合取范式（CNF）公式, 赋值空间, 翻转控制参数, 可满足解

Abstract:

To analyze the structural properties of the CNF (conjunctive normal form) formula??s assignment space under the condition of satisfiability, a parameter[k]is introduced to control the number of times of variable flipping. [k]is not less than 1 and it??s not greater than[n,]where[n]is the number of variable appearing in the formula. Assignment is taken as the node and based on the size of the number of clauses satisfied under the control of the flip boundary, a type of directed graph——BF (bounded flips) graph is introduced. In this paper, some basic properties of BF graphs with flipping control parameters are investigated, and based on this to study the probabilistic properties of satisfiable solutions of CNF formula. It is found that for a CNF formula with[n]variables and[m]clauses, the probability of obtaining a satisfiable solution on the BF graph increases with the increase of flip control parameter[k.]What??s more, when the parameter[k]approaches[n,]the probability is stable. It proves that for a satisfiable CNF formula,[t] steps random walks are performed on BF graphs with arbitrary[k-values.]When[t]is large enough, the probability of obtaining a satisfiable solution will eventually converge to 1. Finally, experimental simulation supports the correctness of the property.

Key words: conjunctive normal form (CNF) formula, assignment space, flip control parameter, satisfiable solution