基于cdcl的sat問題求解算法研究

《基于cdcl的sat問題求解算法研究》由會員上傳分享，免費在線閱讀，更多相關內(nèi)容在學術論文-天天文庫。

1、ｆ駐ｔＥ輪１議議目，Ｓ牛團馳Ｔ耐舊■脯＾鍵．１密級國內(nèi)圖書分類號：０１４１：公開１國際圖書分類號：５０．６西南交通大學研究生學位論文基于ＣＤ化的ＳＡＴ問題求解算法研究年級二零一蘭級姓名易念申請學位級別理學碩±專業(yè)應用數(shù)學指導老師徐揚教授二零一六年五月ＣｌａｓｓｉｆｉｅｄＩｎｄｅｘ：０１４１．１Ｕ．６．Ｄ．Ｃ：５１０ＳｏｕｔｈｗｅｓｔＪｉａｏｉｘｍｇＵｎｉｖｅｒｓｉｔｙＭａｓｔｅｒＤｅｇｒｅｅＴｈｅｓｉｓＳＴＵＤＹＯＮＳＡ

2、ＴＳＬＯＶＩＮＧＡＬＧＯＲＩＴＨＭＢＡＳＥＤＯＮＣＤＣＬＧｒａｄｅ：２０１３Ｃａｎｄｉｄａｔｅ：ＮｉａｎＹｉＡｃａｄｅｍｉｃＤｅｒｅｅＡｌｉｅｄｆｏｒ；ＭａｓｔｅｒｇｐｐＳｅｃｉａｌｉｔ：ＡｌｉｅｄＭａｔｈｅｍａｔｉｃｓｐｙｐｐＳｕｅｒｖｉｓｏｒ：Ｐｒｏｆ．ＹａｎＸｕｐｇＭａｙ，２０１６西南交通大學學位論文版權(quán)使用授權(quán)書本學位論文作者完全了解學校有關保留、使用學位論文的規(guī)定，同意學校保留并向國家有關部口或機構(gòu)送交論文的復印件和電子版，允許論文被查閱和

3、借閱。本人授權(quán)西南交通大學可Ｗ將本論文的全部或部分內(nèi)容編入有關數(shù)據(jù)庫進行檢索，可ｙ？采用影印、縮印或掃描等復印手段保存和匯編本學位論文。本學位論文屬于１□．保密，在年解密后適用本授權(quán)書；２．不保密？吏用本授權(quán)書。＂＂請在上方框內(nèi)打Ｖ（）學位論文作者簽名：指導老師簽名：＾．曰期曰期：ｙ／／／：ｆ：／廠。／西南交通大學碩±學位論文主要工作（貢獻）聲明本文針對求解ＳＡＴ問題所做的主要工作和貢獻如下；一１、本文提出種啟發(fā)式策略，根據(jù)所給子句、文字數(shù)量和出現(xiàn)次數(shù)，定義文字相關系數(shù)，

4、進而對初始變量決策過程提供依據(jù)、子句相關系數(shù)；２，、基于定義的相關系數(shù)給定沖突狀態(tài)定義，根據(jù)沖突狀態(tài)下的總的沖突數(shù)不斷減少的原則，，根據(jù)沖突穩(wěn)定狀態(tài)制定回溯回退機制策略進而定義沖突穩(wěn)定狀態(tài)；［ＷＤＣＬ－３、基于上兩種策略，結(jié)合Ｃ求解器形成求解ＳＡＴ問題新算法Ｃｏｎｆｌｉｃｔ（ＳＡＴ），并采用ＳＡＴ競賽中的問題及ＴＰＴＰ問題庫中旅行商問題進巧實例測試，發(fā)現(xiàn)Ｃｏｎｆｌｔ－ｉｃＳＡＴ算法具有較高的求解效率，對于成功求解的ＳＡＴ問題使用的平均時間較短。本人鄭重聲明，：所呈交的學位論文是在導師指導下獨立進行研

5、究工作所得的成果。除文中己經(jīng)注明引用的內(nèi)容外，本論文不包含任何其他個人或集體已經(jīng)發(fā)表或撰寫過的研究成果。對本文的研究做出貢獻的個人和集體，均己在文中作了明確說明。本人完全了解違反上述聲明所引起的一切法律責任將由本人承擔。學位論文作者簽名：．Ｌ瓜曰期：西南交通大學碩±研究生學位論文第Ｉ頁摘要人工智能領域中，研究命題邏輯公式的可滿足性巧ＡＴ問題具有十分重耍的作用。）隨著科學、技術、社會等領域的發(fā)展，需要解決的ＳＡＴ問題的規(guī)模變得越來越大，而傳統(tǒng)單一的算法無法適應這些大規(guī)模的一些針對大規(guī)

6、模的ＳＡＴ問題的ＳＡＴ問題。因此求解器應運而生，如Ｃｈａｆ、ｚＣｈａｆ、Ｍｉｎｉｓａｔ、Ｌｉｎｇｅｌｉｎｇ等諸多著名求解器。這些求解一器都并非由單的算法構(gòu)建一，而是在傳統(tǒng)的ＤＰＬＬ等算法的基礎上構(gòu)建的套系統(tǒng)，如ＣＤＣＬ求解器，其包含多個決策過程，在算法過程中不斷的改進學習和調(diào)整，Ｗ更為高效的解大規(guī)模的ＳＡＴ問題。送些求解器主要分為如下幾個部分，分別是變量決策、沖突分析、子句學習和回溯機制。而其中的變量決策過程在整個算法構(gòu)架中占有十分一重要的地位，個好的變量決策策略可Ｗ減少沖突的產(chǎn)生，大量節(jié)省求解時間，因

7、此研究變量決策過程的策略具有較為重耍的意文。本文主要結(jié)合ＣＤＣＬ求解器構(gòu)架，做了如下幾個方面的研究工作：一１、本文提出種啟發(fā)式策略，根據(jù)所給子句、文字數(shù)量和出現(xiàn)次數(shù)，定義文字相關系數(shù)，、子句相關系數(shù)進而對初始變量決策過程提供依據(jù)；２、基于定義的相關系數(shù)，給定沖突狀態(tài)定義，根據(jù)沖突狀態(tài)下的總的沖突數(shù)不斷，減少的原則，進而定義沖突穩(wěn)定狀態(tài)根據(jù)沖突穩(wěn)定狀態(tài)制定回溯回退機制策略；３Ｌ－、基于Ｗ上兩種策略，結(jié)合ＣＤＣ求解器形成求解ＳＡＴ問題新算法ＣｏｎｆｌｉｃｔＳＡＴ，（）并采用ＳＡＴ競賽中的問題Ｗ及ＴＰ

8、ＴＰ問題庫中旅行商問題進行實例測試，并對測試結(jié)果進行分析比較。：－命題邏輯，可滿足性問題，，ｔ關鍵字，ＤＰＩＸ算法ＣＤＣＬＣｏｎｆｌｉｃＳＡＴ西南交通大學碩±硏究生學位論文第ＩＩ頁ＡｂｓｔｒａｃｔＴｈｅｓａｔｉｓｆｉａｂｉｌｉｔｙＳＡＴｐｒｏｂｌｅｍ