【摘要】：為解決可滿足性(satisfiability problem,SAT)問題求解過程中分支決策效率不高的問題,提出了一種基于邏輯演繹分組(logical deduction group,LDG)的啟發(fā)式完全算法.該算法通過選擇剩余未滿足子句參與邏輯演繹,得到一組局部可滿足賦值序列,并引導(dǎo)求解器優(yōu)先搜索賦值序列所在解空間;對于可滿足問題,可以通過迭代調(diào)用演繹過程,將局部可滿足解成組地擴充為全局可滿足解,對于不可滿足問題,如果演繹結(jié)果出現(xiàn)空子句,則可以直接判定.采用SAT國際競賽的實例,與具有代表性的指數(shù)級變元狀態(tài)獨立下降和(exponential variable state independent decaying sum,EVSIDS)變量決策算法進行了對比測試,結(jié)果表明:在求解總問題數(shù)方面,LDG比EVSIDS多出42個;在求解速度方面,LDG對可滿足問題的求解時間相較EVSIDS平均減少了22.8%,對不可滿足問題的求解時間平均減少了17.8%,總平均時間減少了20.1%.
[Abstract]:A heuristic complete algorithm based on logical deductive grouping (logical deduction) is proposed to solve the problem of low branch decision efficiency in the process of solving satisfiability problem. By selecting remaining unsatisfied clauses to participate in logical deduction, the algorithm obtains a set of locally satisfiable assignment sequences, and leads the solver to search the solution space of assignment sequences first. The locally satisfiable solution is extended to a global satisfiable solution in groups. For the unsatisfiable problem, if there is an empty subsentence in the deductive result, it can be judged directly. An example of SAT international competition is used to compare it with the representative exponential variable state independent descent and (exponential variable state independent decaying sum EVSIDS variable decision making algorithm. The results show that there are 42 more LDGs than EVSIDS in solving the total number of problems. In terms of solving speed, the average time for solving satisfiable problems is 22.8 less than that for EVSIDS, the average time for solving unsatisfiable problems is 17.8, and the total average time is 20.1.
【作者單位】： 西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院;西南交通大學(xué)系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室;
【基金】：國家自然科學(xué)基金資助項目(61673320,11526171,61305074) 中央高�；究蒲袠I(yè)務(wù)費專項資金資助項目(2682017ZT12)
【分類號】：TP301.6

【相似文獻】

相關(guān)期刊論文 前10條

1 許可,李未;SAT問題的相變現(xiàn)象[J];中國科學(xué)E輯:技術(shù)科學(xué);1999年04期

2 李厚銀;許道云;萬武族;;求解SAT問題的線性半定規(guī)劃算法[J];計算機與數(shù)字工程;2009年11期

3 熊偉;唐璞山;;一種新的SAT問題預(yù)處理算法[J];微電子學(xué)與計算機;2007年10期

4 毛道曉;徐克林;張志英;侯麗清;;越庫中心選址模型與啟發(fā)式算法[J];中南大學(xué)學(xué)報(自然科學(xué)版);2013年02期

5 李克文,吳孟達,張雄明;約簡的一種啟發(fā)式算法[J];計算機工程與科學(xué);2004年01期

6 宋萬忠;;一種改進的多機場地面等待啟發(fā)式算法[J];計算機應(yīng)用;2007年S1期

7 周旭東;王麗愛;陳];;啟發(fā)式算法求解最大團問題研究[J];計算機工程與設(shè)計;2007年18期

8 李亞志;朱夏;;基于插入-分段的無等待流水作業(yè)調(diào)度復(fù)合啟發(fā)式算法[J];東南大學(xué)學(xué)報(自然科學(xué)版);2013年03期

9 唐立新;祁慧;楊自厚;王夢光;;基于P-中位模型的聚類分析的拉格朗日啟發(fā)式算法[J];模式識別與人工智能;1997年01期

10 張潛,高立群,劉雪梅,胡祥培;定位-運輸路線安排問題的兩階段啟發(fā)式算法[J];控制與決策;2004年07期

相關(guān)會議論文 前5條

1 熊偉;唐璞山;;一種新的SAT問題預(yù)處理算法[A];2007年全國開放式分布與并行計算機學(xué)術(shù)會議論文集(下冊)[C];2007年

2 劉嘉敏;馬廣煜;黃有群;;基于組合的三維集裝箱裝入啟發(fā)式算法的研究[A];全國第13屆計算機輔助設(shè)計與圖形學(xué)（CAD/CG）學(xué)術(shù)會議論文集[C];2004年

3 劉金朋;魏長江;;啟發(fā)式算法求最短路徑的一種高效率實現(xiàn)方法[A];2007北京地區(qū)高校研究生學(xué)術(shù)交流會通信與信息技術(shù)會議論文集（上冊）[C];2008年

4 范敏;鄒平;朱興東;;一種啟發(fā)式離散化算法及其Delphi實現(xiàn)[A];第二屆中國智能計算大會論文集[C];2008年

5 馮德鴻;唐加福;郭琦;李輝;;訂貨批量問題改進的相關(guān)策略啟發(fā)式算法與仿真分析[A];2007系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會議論文集[C];2007年

相關(guān)博士學(xué)位論文 前4條

1 賴向京;原子團簇結(jié)構(gòu)預(yù)測的現(xiàn)實途徑—高性能啟發(fā)式算法[D];華中科技大學(xué);2012年

2 黎展滔;具有成組約束的柔性流水車間作業(yè)計劃制定的啟發(fā)式算法[D];廣東工業(yè)大學(xué);2012年

3 董興業(yè);啟發(fā)式算法及其在同順序流水作業(yè)問題中的應(yīng)用[D];北京交通大學(xué);2008年

4 古繼興;KOD多播技術(shù)與Steiner樹啟發(fā)式算法[D];上海交通大學(xué);2007年

相關(guān)碩士學(xué)位論文 前10條

1 周書橙;護士排班的啟發(fā)式算法研究與排班管理系統(tǒng)的設(shè)計實現(xiàn)[D];北京交通大學(xué);2016年

2 劉賽賽;基于增強學(xué)習(xí)的啟發(fā)式和元啟發(fā)式搜索的參數(shù)調(diào)優(yōu)策略[D];電子科技大學(xué);2016年

3 劉志宏;合同組批系統(tǒng)中優(yōu)化算法的研究[D];東北大學(xué);2013年

4 陳濤;基于大數(shù)據(jù)和混合啟發(fā)式算法的公交調(diào)度方法[D];杭州電子科技大學(xué);2016年

5 劉永凱;課表安排問題的啟發(fā)式算法研究[D];廈門大學(xué);2009年

6 陳雪瑛;基于啟發(fā)式算法的庫存路徑優(yōu)化問題研究[D];北京交通大學(xué);2008年

7 陳敏;基于啟發(fā)式算法的合同組批系統(tǒng)研究與設(shè)計[D];東北大學(xué);2012年

8 于U，

本文編號：2142096