發(fā)布時間：2017-11-02 18:38

  本文關鍵詞：求解#SMT問題的局部搜索算法

  更多相關文章： #SMT 滿足性 差分進化 線性公式

【摘要】：#SMT問題是SMT問題的擴展,它需要計算一階邏輯公式F所有可滿足解的個數(shù).目前,該問題已被廣泛應用于編譯器優(yōu)化、硬件設計、軟件驗證和自動化推理等領域.隨著#SMT問題的廣泛應用,設計可以求解較大規(guī)模#SMT實例的求解器亟待解決.基于以上原因,設計了一種求解較大規(guī)模#SMT實例的近似求解器——Vol Compute With Local Search.它在現(xiàn)有的#SMT精確求解算法的基礎上加入差分進化算法,通過調用體積計算工具qhull,進而給出#SMT問題的近似解.算法采用群體規(guī)則減少體積計算的次數(shù),差分進化方法快速地枚舉各個有解的區(qū)域.另外,從理論上證明了Vol Compute With Local Search求解器可以得到精確解的下界,使其可以應用在軟件測試等只需要知道問題下界的領域.實驗結果表明:Vol Compute With Local Search求解器是穩(wěn)定的、具有快速的求解能力,并在高維問題上具有很好的表現(xiàn).
【作者單位】： 東北師范大學計算機科學與信息技術學院;
【關鍵詞】： #SMT 滿足性 差分進化 線性公式
【基金】：國家自然科學基金(61370156,61403076,61403077) 高等學校博士學科點專項科研基金(20120043120017) 新世紀優(yōu)秀人才支持計劃(NCET-13-0724) 吉林省大型科學儀器裝備共享共用專項項目(20150623024TC-03)~~
【分類號】：TP18
【正文快照】： 命題可滿足性問題(簡稱SAT問題)是計算機科學領域的重要研究問題之一,作為第一個被證明為NP完全的問題[1],許多實際問題如電路設計、自動定理證明、限界模型檢驗、等價性檢查都可以在多項式時間內轉為SAT問題進行求解.但由于SAT問題以命題邏輯公式為處理對象,制約了其描述能力

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 吳燕玲;盧建剛;孫優(yōu)賢;;基于免疫原理的差分進化[J];控制與決策;2007年11期

2 楊啟文;蔡亮;薛云燦;;差分進化算法綜述[J];模式識別與人工智能;2008年04期

3 許小健;黃小平;錢德玲;;自適應加速差分進化算法[J];復雜系統(tǒng)與復雜性科學;2008年01期

4 寧桂英;周永權;;基于優(yōu)進策略的新差分進化算法動力學模型參數(shù)的估計[J];計算機與應用化學;2008年05期

5 譚躍;譚冠政;涂立;;一種新的混沌差分進化算法[J];計算機工程;2009年11期

6 王培崇;錢旭;王月;虎曉紅;;差分進化計算研究綜述[J];計算機工程與應用;2009年28期

7 肖術駿;朱學峰;;一種改進的快速高效的差分進化算法[J];合肥工業(yè)大學學報(自然科學版);2009年11期

8 周蕭;王萬良;徐新黎;;解決作業(yè)車間調度問題的混合差分進化算法[J];輕工機械;2010年05期

9 王艷宜;;改進差分進化算法及其應用[J];機械設計與研究;2010年05期

10 張照生;羅健旭;;基于差分進化算法的模糊神經(jīng)網(wǎng)絡控制器[J];計算機與應用化學;2011年12期

中國重要會議論文全文數(shù)據(jù)庫 前5條

1 陸絲馨;肖健梅;王錫淮;;基于改進差分進化算法的艦船電網(wǎng)重構[A];第二十九屆中國控制會議論文集[C];2010年

2 張倩;李海港;;多目標問題的差分進化算法研究[A];2009年中國智能自動化會議論文集（第一分冊）[C];2009年

3 劉國帥;楊侃;陳靜;周景舒;周冉;鄭姣;;差分進化算法在三峽電站廠內經(jīng)濟運行中的應用[A];中國水文科技新發(fā)展——2012中國水文學術討論會論文集[C];2012年

4 倪惠康;杜文莉;錢鋒;;基于改進差分進化算法的PID參數(shù)優(yōu)[A];2009年中國智能自動化會議論文集（第一分冊）[C];2009年

5 雍龍泉;;求解一類多目標優(yōu)化問題的極大熵差分進化算法[A];2013年中國智能自動化學術會議論文集（第五分冊）[C];2013年

中國博士學位論文全文數(shù)據(jù)庫 前10條

1 孫浩;差分進化多目標優(yōu)化算法及其在鋁熱連軋軋制規(guī)程中應用[D];燕山大學;2015年

2 謝宇;差分進化的若干問題及其應用研究[D];南京理工大學;2015年

3 劉榮輝;多階段自適應差分進化算法及應用研究[D];東華大學;2012年

4 王旭;改進差分進化算法及其在可逆邏輯綜合中的應用[D];東華大學;2013年

5 董明剛;基于差分進化的優(yōu)化算法及應用研究[D];浙江大學;2012年

6 丁青鋒;基于元胞自動機的差分進化算法及其在通信系統(tǒng)中的應用研究[D];上海大學;2015年

7 徐斌;基于差分進化算法的多目標優(yōu)化方法研究及其應用[D];華東理工大學;2013年

8 解為成;基于局部摸索的差分進化算法及其在曲面重建中的應用[D];武漢大學;2013年

9 孫成富;差分進化算法及其在電力系統(tǒng)調度優(yōu)化中的應用研究[D];華中科技大學;2010年

10 向萬里;混合群體智能優(yōu)化算法及應用研究[D];天津大學;2014年

中國碩士學位論文全文數(shù)據(jù)庫 前10條

1 萬婧;基于離散微粒群算法和混合差分進化算法的復雜生產(chǎn)調度問題求解[D];昆明理工大學;2015年

2 程菲;膜計算在數(shù)值優(yōu)化問題中的應用研究[D];西華大學;2015年

3 袁文龍;基于控制思想的差分進化算法改進研究[D];東北大學;2014年

4 劉文壯;基于差分進化的約束求解算法研究[D];吉林大學;2016年

5 唐亞;差分進化算法的改進及其在聚類中的應用[D];廣東工業(yè)大學;2016年

6 張轉;基于差分進化算法的混凝土德拜模型的研究[D];長安大學;2015年

7 寧桂英;差分進化算法及其應用研究[D];廣西民族大學;2008年

8 劉俊梅;混合差分進化算法及應用研究[D];北方民族大學;2010年

9 王洪波;基于差分進化計算的聚類算法研究[D];山東師范大學;2012年

10 呼忠權;差分進化算法的優(yōu)化及其應用研究[D];燕山大學;2013年

，

本文編號：1132702