计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2011年
5期
811-822
,共12页
SAT%QBF%求解算法%模型检验%形式化验证
SAT%QBF%求解算法%模型檢驗%形式化驗證
SAT%QBF%구해산법%모형검험%형식화험증
近10年来,布尔可满足性(SAT)求解技术飞速发展,并已经成功应用于模型检验、定理证明等领域,特别是在限界模型检验(BMC)中取得了明显的进展,然而,由于命题逻辑公式的长度随系统规模指数倍增长,基于SAT的模型检验仍然存在状态空间爆炸问题.带量词的布尔公式(QBF)作为SAT公式的自然扩展,具有紧凑的空间结构、更强大、更直观的表达能力,能够简洁地描述模型检验中的公式.基于QBF的模型检验有希望缓解状态空间爆炸问题,成为当前研究的一个热点.总结了当前主流的QBF求解算法及常用的优化技术,指出了该领域中值得关注的新趋势.
近10年來,佈爾可滿足性(SAT)求解技術飛速髮展,併已經成功應用于模型檢驗、定理證明等領域,特彆是在限界模型檢驗(BMC)中取得瞭明顯的進展,然而,由于命題邏輯公式的長度隨繫統規模指數倍增長,基于SAT的模型檢驗仍然存在狀態空間爆炸問題.帶量詞的佈爾公式(QBF)作為SAT公式的自然擴展,具有緊湊的空間結構、更彊大、更直觀的錶達能力,能夠簡潔地描述模型檢驗中的公式.基于QBF的模型檢驗有希望緩解狀態空間爆炸問題,成為噹前研究的一箇熱點.總結瞭噹前主流的QBF求解算法及常用的優化技術,指齣瞭該領域中值得關註的新趨勢.
근10년래,포이가만족성(SAT)구해기술비속발전,병이경성공응용우모형검험、정리증명등영역,특별시재한계모형검험(BMC)중취득료명현적진전,연이,유우명제라집공식적장도수계통규모지수배증장,기우SAT적모형검험잉연존재상태공간폭작문제.대량사적포이공식(QBF)작위SAT공식적자연확전,구유긴주적공간결구、경강대、경직관적표체능력,능구간길지묘술모형검험중적공식.기우QBF적모형검험유희망완해상태공간폭작문제,성위당전연구적일개열점.총결료당전주류적QBF구해산법급상용적우화기술,지출료해영역중치득관주적신추세.
