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

项目名称： 极小不可满足公式的结构与分类

项目编号： No.61272059

项目类型： 面上项目

立项/批准年度： 2013

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

项目作者： 赵希顺

作者单位： 中山大学

项目金额： 70万元

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

中文关键词： 可满足(SAT)问题；极小不可满足公式；公式结构；公式分类；表达能力

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

英文关键词： the satisfiability problem；minimal unsatisfiable formula；structure of formulas；classification of formulas；expressive power