带正则结构的命题公式的可满足性问题研究

Each clause contains exactly k literals and each variable occurs exactly s times in a regular (k,s)-CNF formula. The complexity of decision problem for satisfibility remains NP-completeness for some subclasses of regular formulas, such as (3,4)-SAT is NP-complete，which we have shown that a 3-CNF formula can be reduced polynomially to a regular (3,4)-CNF formula. The factor graph of a regular (k,s)-CNF formula is a regular bigraph, in which the degree of each variable node is exactly s, and the degree of clause node is exactly k. The regular bigraph has some well results and properties in theory of graph. These results and properties will be useful for investigating satisfiability of (k,s)-CNF formulas. We will get properties of some parameters effecting satisfiability of regular formulas, and these properties are helpful for analyzing satisfiability of k-CNF formulas. . In this project, we focus on researching the satisfibility problem of propositional formulas with regular structures. It includes .(a) investigating structures, properties, and applications of inapproximability of regular formulas; properties of expander coefficients and applications to design and analysis of random algorithms for SAT problem;.(b) optimizing algorithms for MAX (k,s)-SAT based on properties and estimation of bound of of expander coefficients in regular bigraphes; .(c) presenting random models producing (k,s)-CNF formulas and analyzing distribution of satisfiable resolutions, complexity and critical properties of random (k,s)-SAT based on properties of regular bigaphes from regular formulas;.(d) researching parameterized complexity for (k,s)-SAT, considering whether or not one can get tractable formulas by deleting at most t variable nodes (resp. clause nodes, mixed nodes, edges with sign labels ) from original regular formulas; .(e) investigating information passing algorithms for (k,s)-SAT, and analyzing the convergence of algorithms constrainting inputs to (k,s)-CNF formulas.

正则（k,s）-CNF公式中每个子句的长度恰为k，每个变元出现的次数恰为s。在某些正则公式类中，SAT问题仍然是NP完全问题。如：（3,4）-SAT是NP完全问题。本项目研究带正则结构的命题公式的可满足性问题。研究内容包括：正则（k,s）-CNF公式的结构和性质分析，（k,s）-SAT问题的不可近似性质及其应用；（k,s）-CNF公式因子图的膨胀系数性质以及在SAT问题随机算法设计与分析中的应用，基于对膨胀系数界的估计，研究MAX（k,s）-SAT优化算法；基于（k,s）-CNF公式因子图的正则性质，研究随机（k,s）-CNF公式的随机生成模型、以及随机（k,s）-SAT问题解的分布与相变性质；（k,s）-SAT问题的固定参数复杂性，删去至多t个（变元结点、子句结点、交叉结点）或t条（标记）边后，公式是否退化到易解类的固定参数复杂性；信息传播算法求解（k,s）-SAT问题及算法收敛性分析。

在本项目主要研究带有规则结构的可满足性问题的结构性质和相变性质其主要成果包括：. 找到一个具有良好正则性质并保留NP完全性的CNF公式子类---正则（3,4）-CNF，在此类CNF公式中，每个子句的长度恰为3，每个变元出现的次数恰为4。. 研究了信息传播算法的收敛性。对于警示传播算法，给出了随机k-CNF 公式因子图上圈存在的相变点,将警示信息的取值从{0,1}松弛为[0,1],给出了WP 算法收敛的一个充分条件。对于置信传播算法，对在RB模型生成的实例上收敛进行了研究，并得到一些有用的收敛参数。. 围绕随机正则公式的难解实例结构特征、实例生成模型、相变现象等方面对随机正则公式的可满足性问题进行展开研究。提出了一种新的随机正则（k,r）-CNF公式实例生成模型——GRR(N,k,r)模型和随机正则(3,r)-CNF公式的实例生成模型——GRR3(N,r)模型。实验表明：随着r的逐渐增大，求解GRR3(N,r)模型所生成的随机正则(3,r)-CNF问题实例的难度也会呈现 “Easy-Hard-Easy”模式，且随机正则(3,r)-SAT问题的实验相变点位于r=11处（约束密度约为3.667）。 实验表明：求解GRR(N,k,r)模型所产生的随机正则（3,11）-CNF公式通常远比求解随机3-SAT问题实例生成模型所产生的约束密度为4.267附近的3-CNF公式难，即GRR3(N,r)模型能够产生更难解的随机3-SAT问题实例。. 利用组合分析技术中概率生成函数的系数近似技术，给出了当前随机正则(3,r)-SAT问题可满足临界值的最好上界，即当一个随机正则(3,r)-CNF公式F中的变元出现次数r>11时，F以高概率不可满足。进一步，得到了随机正则(k,r)-SAT问题可满足临界值点的一个新的上界，并且使得上、下界之间仅相差一个常数1+3ln2/2。基于格局模型技术，通过构造一个特殊的独立随机试验来模拟随机公式F中所有文字的分布情况，得到了与基于生成函数系数近似技术相一致的随机正则(k,r)-SAT问题可满足临界值的上界。