命题公式有效推理的特殊变元集及算法研究

项目名称： 命题公式有效推理的特殊变元集及算法研究

项目编号： No.60863005

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

立项/批准年度： 2009

项目学科： 金属学与金属工艺

项目作者： 许道云

作者单位： 贵州大学

项目金额： 26万元

中文摘要： 本项目研究成果主要包括：(1) 特殊结构命题公式类的性质及判定问题。系统地研究了著名难例鸽巢公式的若干结构性质，找到了最大可满足指派的两种标准范式。如果允许对同构公式的结点使用剪枝规则，给出了在三次方时间内对鸽巢公式不可满足性验证的算法。研究了CNF公式的Horn子结构对公式本身可满足性的影响，引入最大可改名Horn子结构与最小不可嵌入Horn子结构两种方法研究CNF公式的可满足性。给出了将CNF公式类多项式时间归约到规则结构类的技术，为在规则结构下研究SAT问题提供了理论基础。（2）利用特殊变元集（关键文字集、后门集）研究CNF公式的可满足性和有效推理，提出了特殊变元集的计算方法，研究了关键文字集与极小不可满足公式之间的内在联系，应用特殊变集的特殊性设计求解SAT问题的算法。研究了信息传播算法在特殊变元集计算中的应用、以及信息传传播算法算法的收敛性。（3）给出了二元关系性质测试算法和复杂性分析，深入研究了布尔函数的学习与性质测试的理论，其理论和方法可以用到机器学习的算法理论、协调检测理论和算法设计。

中文关键词： 命题公式;特殊变元集;结构性质;算法设计;信息传播算法;性质测试与分析。

英文摘要： In this project, it is finished works including that: (1) The properties and complexies of decision problems in classes of propositional formulas with special sturstures have been investigated. We research systematically properties of structures in the pigeon-hole formulas, which is a class of famous hard instances for resolution, and find two normal forms of assignments satisfying maximum of clauses in the formula, and present an algorithm to check unsatisfiability of pigeon-hole formulas, which the complexity is cubic time of number of varables occurring in formula if the isomorphism rules could be used in the algorithm to trim one of branches labled by isomorphic formulas. We also research the effect of Horn structures to satisfiability for CNF formulas, and investigate satisfiability of CNF formulas by introducing maximal renameable Horn subformulas and minimal unembedded Horn sets. We present a method to reduce polynomially a CNF formula to a regular CNF formula, and then find a basic thoery to research satisfiability for regular NP-complete problems. (2) The sets of sepcial variables including key literal sets and backdoor sets are applied to researching satisfiability and effective inference for CNF formulas. We present some algorithms computing sets of sepcial variables, and find some inherent relations between sepcial variables and minimal unsatisfiable formulas, and apply properties of special variables to designing algorithms for solving SAT problems. We also apply information passing algorithms to computing sets of sepcial variables, and resarch convergence of the algorithm. (2) We present some algorithms for testing properties of binary relations and analyze complexities of algorithms, and research deeply theory of learning and testing for Boolean functions. The theory and method can be used to machine learning and association checking.

英文关键词： propositional formula;The sets of sepcial variables;structure property;algorithm design;information passing algorithm;test and analysis of properties.