SAT求解局部搜索行為分析與概率控制策略.pdf

1、SAT問(wèn)題(Satisfiability problem)，是第一個(gè)被證明的NPC(Non-deterministic Polynomial Complete)問(wèn)題，在計(jì)算機(jī)科學(xué)理論和應(yīng)用中具有重要的意義。對(duì)于理論研究，它是計(jì)算復(fù)雜性理論的奠基石，所有的NPC問(wèn)題都可以在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)化為SAT問(wèn)題。對(duì)于工業(yè)應(yīng)用，SAT可用于解決等價(jià)性驗(yàn)證、有界模型檢測(cè)、電子設(shè)計(jì)自動(dòng)化、統(tǒng)計(jì)物理學(xué)等多方面問(wèn)題。因此，高效實(shí)用的SAT算法和技術(shù)是目前研究

2、的熱點(diǎn)。
　　局部搜索算法是目前求解SAT問(wèn)題比較有效的算法，Sattime算法是典型的局部搜索算法，曾在2011年的SAT問(wèn)題國(guó)際求解大賽中獲得隨機(jī)類(lèi)型算例組的銀牌。它是基于Novelty系列的算法，在選擇翻轉(zhuǎn)變?cè)獣r(shí)它利用了子句滿(mǎn)足的歷史信息，對(duì)其求解過(guò)程進(jìn)行行為分析與模式挖掘可以發(fā)現(xiàn)變?cè)c子句間蘊(yùn)含的因果關(guān)系。建立數(shù)據(jù)庫(kù)記錄局部搜索算法的求解行為，對(duì)翻轉(zhuǎn)事件進(jìn)行數(shù)據(jù)挖掘，包括關(guān)聯(lián)規(guī)則模式挖掘和頻繁序列模式挖掘。通過(guò)對(duì)挖掘結(jié)果進(jìn)

3、行分析，發(fā)現(xiàn)Sattime算法有時(shí)會(huì)出現(xiàn)先后選擇同一個(gè)變?cè)默F(xiàn)象，這種現(xiàn)象可能使搜索過(guò)程產(chǎn)生回環(huán)。從而提出兩種概率控制策略：加強(qiáng)子句選擇策略和加強(qiáng)變?cè)x擇策略。將這兩種策略應(yīng)用到Sattime算法中，形成新的局部搜索算法Sattime-P。
　　使用Sattime算法和Sattime-P算法對(duì)不同類(lèi)型的算例進(jìn)行求解，對(duì)比它們的平均翻轉(zhuǎn)次數(shù)、平均求解時(shí)間。實(shí)驗(yàn)結(jié)果表明使用改進(jìn)策略的Sattime-P算法在大多數(shù)情況下減少了平均翻轉(zhuǎn)次