智能系统学报Issue(6)：497-504,8.DOI:10.3969/j.issn.1673-4785.201212058
不可满足子式研究
Research on an unsatisfiable subformula
摘要
Abstract
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 pro-grams , and design and verification of hardware and software .An unsatisfiable subformula may be very helpful in di-agnosing 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 subfor-mula , introduce the subcategory of an unsatisfiable subformula from the viewpoint of calculation complexity , param-eter complexity and the research on an unsatisfiable subformula in QBF .Finally, the authors discuss the future di-rection of research on an unsatisfiable subformula .关键词
可满足性问题/不可满足子式/可满足模理论/局部搜索Key words
satisfiability problem/unsatisfiable subformula/satisfiability module theory/local search分类
信息技术与安全科学引用本文复制引用
殷明浩,李欣..不可满足子式研究[J].智能系统学报,2013,(6):497-504,8.基金项目
国家自然科学基金资助项目（61070084，60803012）． （）
