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

摘要：

为分析合取范式（conjunctive normal form，CNF）公式的赋值空间在可满足性情况下的结构性质，引入一个变元翻转次数控制的参数[k, k]不小于1且不大于[n, n]为公式中出现的变元个数，以赋值作为结点，基于翻转界控制下赋值满足子句数的大小，引入一类有向图——BF（bounded flips）图。研究带翻转控制参数的BF图的若干基础性质，根据BF图的性质研究CNF公式可满足解的概率性质。对于含有[n]个变元[m]个子句CNF公式，随着翻转控制参数[k]的增大，在其BF图上取得可满足解的概率也相应增大。当[k]靠近[n]时，概率稳定。对于可满足的CNF公式，在其任意[k]值下的BF图上进行[t]次随机游走。当[t]足够大时，取得可满足解的概率最终会收敛于1。最后，实验仿真支持性质的正确性。

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