d-正则命题公式的可满足问题研究

In a regular (k,r)-CNF formula F, each clause contains exactly k literals and each variable occurs exactly r times in the formula. A formula is d-regular if the formula is a regular (k,r)-CNF formula for some positive integers k and r, and the difference of numbers of times that each variable occurs positively and negatively in the formula is less than d, where d is a nonnegative integer. Specially, the formula is called balance regular formula if d=0. It is known that the regular (3,4)-SAT problem is NP-complete. We note that the ratio of clause number to variable number in the regular (3,4)-CNF formula is a constant 4/3, which is far away the classical phase transition point 4.29 for random 3-SAT problem. It means that there exists still the hard-zone in the classical “easy-field”, and such hard instances have regular structures. .In this project, we will focus on investigating the satisfiability problem for d-regular propositional formulas by controlling parameters k, r and d, where parameters k and r are used to control regular structure, and the parameter d is used to control difference of positive\negative occurrences of variables. The research includes：. (1) Investigating satisfiability problems for balance regular (k,2r)-CNF formulas.. (2) Theory search of hard solutions of satisfiability for d-regular CNF formulas.. (3) Investigating phase transformation of random d-regular satisfiability problems.. (4) Investigating convergence of the message propagation algorithms for balance d-regular instances.. (5) Investigating structure and properties of solutions under regular reduction transformations.

在d-正则（k,r）-CNF公式中，每个子句长度恰为k，每个变元出现次数恰为r，每个变元正负出现次数的差不超过d。d=0时，正则（k,r）-CNF公式称为平衡正则公式，此时r为一个偶数。己知正则(3,4)-SAT问题NP完全的，正则(3,4）-CNF公式中子句数与变元数的比值恒为一个常数4/3，远离通常的随机3-SAT问题的相变点4.29，此意味着原先理解的“易解区域”内仍有难解地带，并且难解实例具有正则结构。本项目研究d-正则命题公式的可满足性问题，借助正则性控制参数k,r, 变元正负出现次数之差的控制参数d, 在规范结构下研究NP理论。研究内容包括：平衡正则（k,2r）-CNF公式的可满足性问题的结构性质、求解算法及复杂性分析；一般d-正则可满足性问题的难解现象的理论研究、相变性质、难易分界的上、下界估计、以及解的聚类性质；随机d-正则公式实例下信息传播算法的收敛条件和收敛性质

在（s,k）-CNF正则公式中，每个子句的长度为k，每个变元出现的次数均为s。以此类正则结构公式为基础，通过从不同控制参数控制变元正负出现次数，并考虑不同可满足概念，围绕申请书中拟定研究内容，研究正则CNF公式的结构与相变性质；研究正则CNF公式超解下NP完全性和唯一解存在性的临界现象。基于公式的结构熵研究可满足问题的求解算法；研究信息传播算法在NP-难问题的优化求解和解的收敛性质。其主要研究成果包括：.(1). 引入（s,c,k）-CNF正则公式类(0<c<1),参数用于控制正负变元出现比例。 研究（s,c,k）-CNF公式的严格满足性问题（指派使每个子句恰有一个文字为真）。对于此类严格满足性问题，存在一个关于变元出现次数的严格相变s*。研究（s,k）-CNF公式的另一类严格满足性问题（2-严格满足）（指派使每个子句恰有两个文字为真）。对于此类满足性问题，同样存在一个关于变元出现次数的严格相变s*。两类严格满足性问题的严格相变s*，均有确定的数学表达式。实验支持理论研究结果。对于变元的变元正负出现次数参数d，考虑一般可满足性下的d-正则(k,s)问题相变问题。研究表明：控制参数d有严格相变d*,给出了严格相变的数学证明和实验验证。.(2).正则（k,s）-CNF公式的一个(1,0)-超解是一个可满足指派，并且任意一个文字（正-负）翻转后得到的新指派仍然是公式的一个满足指派。研究发现：当k>3时，存在一个关于k的临界函数 ,当 时，公式有(1,0)-超解，当 时，(1,0)-(k,s)-SAT问题是NP完全的。引入变元正负出现次数差的上界控制参数d, d-正则(k,s)-SAT问题的唯一可满足性问题，类似有一个临界函数 区分唯一解的存在性。.(3). 基于公式因子图的结构熵研究SAT问题的求解算法。研究表明：利用公式的结构熵改进初始解的生成、以及指导变元的翻转具有明显效果。.(4). 研究信息传播算法在MAX-SAT问题上的应用，并分析解的收敛性条件；将信息传播算法应用到其它NP-难问题的优化求解问题。引入WP 可解概念，研究WP-可解公式上在警示传播算法收敛的有效条件。得到结论: 对于一个可满足公式，WP-可解当且仅当WP算法高概率收敛。