智能系统学报
智能繫統學報
지능계통학보
CAAI TRANSACTIONS ON INTELLIGENT SYSTEMS
2013年
6期
497-504
,共8页
可满足性问题%不可满足子式%可满足模理论%局部搜索
可滿足性問題%不可滿足子式%可滿足模理論%跼部搜索
가만족성문제%불가만족자식%가만족모이론%국부수색
satisfiability problem%unsatisfiable subformula%satisfiability module theory%local search
为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域，对不可满足子式进行了相关研究。对当前不可满足子式的主要相关算法进行了概述评论、分类归纳，并从计算复杂性角度介绍了其子类、参数复杂性以及QBF中的极小不可满足子式。总结了近10年来不可满足子式的理论与算法，讨论了不可满足子式的未来研究发展方向。研究有利于进一步发现不可满足的根本原因，从而进行有针对性地改进，并对相关人员的研究提供帮助。
為瞭廣汎有效地將不可滿足子式應用于知識驗證、產品規劃、硬件和軟件的設計與驗證等領域，對不可滿足子式進行瞭相關研究。對噹前不可滿足子式的主要相關算法進行瞭概述評論、分類歸納，併從計算複雜性角度介紹瞭其子類、參數複雜性以及QBF中的極小不可滿足子式。總結瞭近10年來不可滿足子式的理論與算法，討論瞭不可滿足子式的未來研究髮展方嚮。研究有利于進一步髮現不可滿足的根本原因，從而進行有針對性地改進，併對相關人員的研究提供幫助。
위료엄범유효지장불가만족자식응용우지식험증、산품규화、경건화연건적설계여험증등영역，대불가만족자식진행료상관연구。대당전불가만족자식적주요상관산법진행료개술평론、분류귀납，병종계산복잡성각도개소료기자류、삼수복잡성이급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 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 .
