首頁 > 期刊 > 自然科學(xué)與工程技術(shù) > 信息科技 > 電子信息科學(xué)綜合 > 計(jì)算機(jī)工程與科學(xué) > 基于一階邏輯的可滿足求解方法研究進(jìn)展 【正文】
基于一階邏輯的可滿足求解方法研究進(jìn)展
張建民; 黎鐵軍; 馬柯帆; 肖立權(quán) 國防科技大學(xué)計(jì)算機(jī)學(xué)院; 湖南長沙410073
- 形式化驗(yàn)證
- 一階邏輯
- 布爾可滿足
- 可滿足性模理論
摘要：基于命題邏輯的布爾可滿足SAT存在描述能力弱、抽象層次低、求解復(fù)雜度高等問題,而基于一階邏輯的可滿足性模理論SMT采用高層建模語言,表達(dá)能力更強(qiáng),更接近于字級設(shè)計(jì),避免將問題轉(zhuǎn)化到位級求解,在硬件RTL級驗(yàn)證、程序驗(yàn)證與實(shí)時(shí)系統(tǒng)驗(yàn)證等領(lǐng)域得到了廣泛應(yīng)用。針對近年來涌現(xiàn)的眾多SMT求解方法,依據(jù)方法的求解方式進(jìn)行了分類與對比。而后,對3種主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的實(shí)現(xiàn)進(jìn)行了概要介紹。最后,討論了SMT求解方法當(dāng)前所面臨的主要挑戰(zhàn)以及在SMT求解方面的一些研究成果,并對今后的研究進(jìn)行了展望。
注：因版權(quán)方要求，不能公開全文，如需全文，請咨詢雜志社
計(jì)算機(jī)工程與科學(xué)
- 預(yù)計(jì)1-3個(gè)月 預(yù)計(jì)審稿周期
- 0.79 影響因子
- 計(jì)算機(jī) 快捷分類
- 月刊 出版周期
主管單位：國防科技大學(xué);主辦單位：國防科技大學(xué)計(jì)算機(jī)學(xué)院
我們提供的服務(wù)
在線客服
一對一咨詢服務(wù)、簡單快捷、省時(shí)省力
了解更多 >
快遞配送
直郵到家、實(shí)時(shí)跟蹤、更安全更省心
了解更多 >
雜志訂閱
去除中間環(huán)節(jié)享受低價(jià)，物流進(jìn)度實(shí)時(shí)通知
了解更多 >
雜志推薦
正版雜志，匹配度高、性價(jià)比高、成功率高
了解更多 >