本文關(guān)鍵詞：求解#SMT問(wèn)題的局部搜索算法

  更多相關(guān)文章： #SMT 滿足性 差分進(jìn)化 線性公式

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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

9 王艷宜;;改進(jìn)差分進(jìn)化算法及其應(yīng)用[J];機(jī)械設(shè)計(jì)與研究;2010年05期

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

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

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

2 張倩;李海港;;多目標(biāo)問(wèn)題的差分進(jìn)化算法研究[A];2009年中國(guó)智能自動(dòng)化會(huì)議論文集（第一分冊(cè)）[C];2009年

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

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

5 雍龍泉;;求解一類多目標(biāo)優(yōu)化問(wèn)題的極大熵差分進(jìn)化算法[A];2013年中國(guó)智能自動(dòng)化學(xué)術(shù)會(huì)議論文集（第五分冊(cè)）[C];2013年

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

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

2 謝宇;差分進(jìn)化的若干問(wèn)題及其應(yīng)用研究[D];南京理工大學(xué);2015年

3 劉榮輝;多階段自適應(yīng)差分進(jìn)化算法及應(yīng)用研究[D];東華大學(xué);2012年

4 王旭;改進(jìn)差分進(jìn)化算法及其在可逆邏輯綜合中的應(yīng)用[D];東華大學(xué);2013年

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

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

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

8 解為成;基于局部摸索的差分進(jìn)化算法及其在曲面重建中的應(yīng)用[D];武漢大學(xué);2013年

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

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

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

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

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

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

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

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

6 張轉(zhuǎn);基于差分進(jìn)化算法的混凝土德拜模型的研究[D];長(zhǎng)安大學(xué);2015年

7 寧桂英;差分進(jìn)化算法及其應(yīng)用研究[D];廣西民族大學(xué);2008年

8 劉俊梅;混合差分進(jìn)化算法及應(yīng)用研究[D];北方民族大學(xué);2010年

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

10 呼忠權(quán);差分進(jìn)化算法的優(yōu)化及其應(yīng)用研究[D];燕山大學(xué);2013年

，

本文編號(hào)：1132702