CAJ | 학술논문

求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点.本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点.最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望.
구해공식적가만족성재제여형식화험증、전자설계자동화여인공지능등음다영역중도구유비상중요적이론여응용개치,성위근년래적연구열점.본문침대명제공식여일계공식적가만족성문제,중점개소료포이가만족성여가만족성모이론구해기술적기본원리,병차근거산법적류형진행분류천술,분석료각충산법적우결점.최후,토론료목전면림적주요도전,대금후적연구방향진행료전망.
Solving the satisfiahility of formulae is theoretically important in the practical applications of various fields,such as formal verification, electronic design automation and artificial intelligence. This paper introduces the principles of the Boolean Satisfiability and Satisfiability Modulo Theories. The existing algorithms are introduced and compared according to their types. The qualities of these algorithms are also analyzed. Finally, we discuss the currem challenges, and outline the future research trend.