不可满足子式研究

Research on an unsatisfiable subformula

为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域,对不可满足子式进行了相关研究.对当前不可满足子式的主要相关算法进行了概述评论、分类归纳,并从计算复杂性角度介绍了其子类、参数复杂性以及QBF中的极小不可满足子式.总结了近10年来不可满足子式的理论与算法,讨论了不可满足子式的未来研究发展方向.研究有利于进一步发现不可满足的根本原因,从而进行有针对性地改进,并对相关人员的研究提供帮助.

In recent years, an increasing number of researchers have started to focus their attention on unsatisfiable subformulas, especially in regards to the extremely small and the minimal unsatisfiable subformulas. The unsatisfi- able subformula （US） has a wide range of practical applications, including knowledge validation, product programs, and design and verification of hardware and software. An unsatisfiable subformula may be very helpful in diagnosing the causes of unfeasibility in large systems. In the past 10 years, research on an unsatisfiable subformula has been developed quickly. In this paper, the authors discuss the algorithm in relation to an unsatisfiable subformula, introduce the subcategory of an unsatisfiable subformula from the viewpoint of calculation complexity, parameter complexity and the research on an unsatisfiable subformula in QBF. Finally, the authors discuss the future di- rection of research on an unsatisfiable subformula.