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

项目名称： 带正则结构的命题公式的可满足性问题研究

项目编号： No.61262006

项目类型： 地区科学基金项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 许道云

作者单位： 贵州大学

项目金额： 46万元

中文摘要： 正则（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问题及算法收敛性分析。

中文关键词： 正则（3;4）-CNF公式；信息传播算法；收敛性；随机正则(3;r)-CNF公式；相变性质

英文摘要： 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 expande

英文关键词： regular (3;4)-CNF formulas；message propagation algorithms；convergence；regular random (3; r)-CNF formulas；phase transition properties