极小不可满足公式的结构与分类

The algorithms for extracting minimal unsatisfiable (MU) subformulas have been utilized more and more in computer sciences, artificial intelligence and other areas. Consequently, the investigation of MU formulas and algorithms for extracting MU subformulas has been becoming an important research direction of SAT problem. However, according to A.Nadel's paper, the existing extracting algorithms cannot meet the practical requirements, they cannot solve practical problems from the industry except for several problem instances. This project aims at structural study of MU formulas in order to provide useful technique and heuristics for optimizing extracting algorithms. We will classify MU formulas by deficiency, the number of occurrences of variables, the number of full clauses, the congruence of DP resolution. In order to give characterization of structures of MU formulas we at first investigate the structure of MU formulas in each class. We hope to find some structural properties which can be decided in polynomial time. On the other hand, this research would provide some theoretical foundation for the further investigation of generalized minimal unsatisfiability (e.g. minimal false quantified Boolean formulas, minimal unsatisfiable linear-temporal formulas, minimal unsatisfiable Boolean circuits).

极小不可满足(MU)子公式提取算法越来越多地应用于计算机科学、人工智能等领域。因此，近年来MU公式及MU子公式提取算法研究已成为SAT问题研究的重要方向。然而，根据A.Nadel的报告，现在的MU子公式提取算法都还没有达到实际应用的要求，目前仅能解决工业上的几个简单问题。本项目试图通过对MU公式结构的研究为MU子公式提取算法提供优化技术或启发信息。我们将根据MU公式的亏度、变元出现的次数、full子句的个数、DP消解的同余性对MU公式进行分类。首先研究各类公式的结构特性，进而刻画MU公式的结构。我们希望找到一些易于判定的结构性质，以便应用于MU子公式提取算法中。另一方面，本课题也将为研究推广了的极小不可满足问题（极小假量化布尔公式、极小不可满足时序逻辑公式、极小不可满足电路）提供理论基础。

本项目主要研究极小不可满足(MU)公式的结构。为此我们研究了不同类型的MU公式。主要研究了MU公式的最小变元度(即变元出现次数最小的上界)、全子句度、公式因子. 研究了它们与non-Mersenne数，Smarandache数之间的紧密联系。同时利用公式的结构性质研究逻辑系统的表达能力与计算复杂性。..本项目共发表论文9篇，主要发表在Theoretical computer Science，Science China，Minds and Machines，Frontiers in Computer Science, 以及顶级国际会议KR2004. 主编亚洲逻辑会议论文集(World Scientific). 另有3篇文章已投Journal of Comuter Science and Systems和Discrete Applied Mathematics等，目前还在审稿过程，其中两篇已有反馈意见. 审稿人对文章给予充分肯定, 例如: This paper is a further step towards developing the theory by considering the combinatorial structure of minimally unsatisfiable formulas. The results of the paper are interesting and they definitely represent progress progress towards developing the theory. I find the results interesting and not only the results but the proof technique as well. The way how measuring the number of full clauses and variable degree is quite novel to me, I think the results certainly deserve publication and they are well-suited for a journal like DAM...通过本项目，已有培养4位博士研究生，2位硕士研究生