可滿足性問題的求解算法和結(jié)構(gòu)性質(zhì)研究是計(jì)算機(jī)科學(xué)中重要問題之一,為尋求某些CNF公式子類問題有效算法或算法改進(jìn)途徑,對(duì)公式的結(jié)構(gòu)加以某些限制,其中限定子句長(zhǎng)度為恒定常數(shù)和變?cè)霈F(xiàn)次數(shù)是常見的處理方式。研究具有正則結(jié)構(gòu)且每個(gè)變?cè)?fù)出現(xiàn)均衡的結(jié)構(gòu)化公式的可滿足性問題求解,其隨機(jī)生成模型的構(gòu)建及隨機(jī)實(shí)驗(yàn)測(cè)試有助于觀察解分布狀況。并且,隨機(jī)局部搜索算法在求解具有一定規(guī)則結(jié)構(gòu)CNF公式實(shí)例中具有良好效率。本文集中研究平衡正則（k,2r）-CNF公式的求解問題,即限制每個(gè)子句的長(zhǎng)度為k,每個(gè)變?cè)霈F(xiàn)的次數(shù)為偶數(shù)2r,并且每個(gè)變?cè)?fù)出現(xiàn)的次數(shù)在相等情況下的可滿足性問題求解。給出BR（n,k,2r）模型,以此模型來生成具有特殊結(jié)構(gòu)的平衡正則（k,2r）-CNF公式實(shí)例,利用隨機(jī)局部搜索算法求解問題。通過限制初始指派的0文字和1文字各占一半且均勻生成,以Walk SAT算法和NSAT算法做實(shí)驗(yàn)對(duì)比,發(fā)現(xiàn)對(duì)于平衡正則（k,2r）-CNF公式,實(shí)例具有明顯效率。 

【文章來源】：計(jì)算機(jī)與現(xiàn)代化. 2019,(01)

【文章頁(yè)數(shù)】：5 頁(yè)

【部分圖文】：

初始指派被限制的實(shí)例類ＲegFormula-5000-3-8在SLS算法下的求解時(shí)間

【參考文獻(xiàn)】：
期刊論文
[1]基于人工智能路徑規(guī)劃系統(tǒng)的智能小車的設(shè)計(jì)與實(shí)現(xiàn)[J]. 蔡莉莎,曾維鵬.  電子世界. 2016(18)
[2]基于加強(qiáng)概率控制策略的SAT局部搜索算法[J]. 洪劍珂,張崢華,許貴平.  計(jì)算機(jī)工程與應(yīng)用. 2017(14)
[3]正則3-SAT問題的相變現(xiàn)象[J]. 張明明,許道云.  計(jì)算機(jī)科學(xué). 2016(04)
[4]極小不可滿足公式在多項(xiàng)式歸約中的應(yīng)用[J]. 許道云.  軟件學(xué)報(bào). 2006(05)
[5]SAT問題中局部搜索法的改進(jìn)[J]. 楊晉吉,蘇開樂.  計(jì)算機(jī)研究與發(fā)展. 2005(01)
[6]AI規(guī)劃的回顧與展望[J]. 劉吉穎,方思行.  中山大學(xué)學(xué)報(bào)論叢. 2000(05)
[7]求解SAT問題的局部搜索算法及其平均時(shí)間復(fù)雜性分析[J]. 劉濤,李國(guó)杰.  計(jì)算機(jī)學(xué)報(bào). 1997(01)

博士論文
[1]自動(dòng)推理與規(guī)劃問題最小上界和相變規(guī)律研究[D]. 周俊萍.吉林大學(xué) 2011

碩士論文
[1]基于FPGA鏌擬的SAT求解方法[D]. 毛樂樂.廣西民族大學(xué) 2016
[2]基于SAT的數(shù)字電路ATPG方法及應(yīng)用[D]. 張?jiān)廊A.吉林大學(xué) 2012
[3]基于SAT的VLSI測(cè)試向量自動(dòng)生成技術(shù)[D]. 付宇.北京交通大學(xué) 2010



本文編號(hào)：3298116