以字符個(gè)數(shù)為參數(shù)的可滿足性問題算法研究

1、中圖分類號(hào)!里3窆3UDC620碩士學(xué)位論文學(xué)校代碼!Q33密級(jí)公開以字符個(gè)數(shù)為參數(shù)的可滿足性問題算法研究AlgorithmResearchonSatisfiabilityProblemParameterizedbyFormulaLength作者姓名：學(xué)科專業(yè)：研究方向：學(xué)院(系、所)：指導(dǎo)教師：副指導(dǎo)教師：徐超計(jì)算機(jī)科學(xué)與技術(shù)計(jì)算機(jī)算法信息科學(xué)與工程學(xué)院陳建二教授王建新教授論文答辯日期壘2盛竭!為答辯委員會(huì)主席垂：魚中南大學(xué)2014年

2、5月萬方數(shù)據(jù)以字符個(gè)數(shù)為參數(shù)的可滿足性問題算法研究摘要：在可計(jì)算性理論和復(fù)雜性理論中，可滿足性問題是一個(gè)重要的NP一完全問題?？蓾M足性問題已經(jīng)廣泛地應(yīng)用于自動(dòng)推演，計(jì)算機(jī)輔助設(shè)計(jì)，計(jì)算機(jī)輔助操作，機(jī)器視覺，數(shù)據(jù)庫等等。通常來說，可滿足性問題是指離散的有約束的一類判定性問題，其形式化定義為：給定一個(gè)布爾合取范式F，是否存在一個(gè)F的賦值，使得F為真。可滿足性問題算法的時(shí)間復(fù)雜度計(jì)算過程主要涉及3類參數(shù)：范式中變量的個(gè)數(shù)孔，范式中子句的個(gè)數(shù)m

3、，范式中字符的個(gè)數(shù)L。本文從字符個(gè)數(shù)L的角度，研究了一般性可滿足性問題的精確算法。在以同樣參數(shù)來解決該問題的精確算法中，目前最好的算法時(shí)間復(fù)雜度為O‘(10652￡)，其中L是范式中字符的個(gè)數(shù)。本文首先研究了可滿足性問題的預(yù)處理過程。根據(jù)消除(resolution)原理和引入的度量一范式F中所有變量的頻率權(quán)值之和，本文給出了12條化簡(jiǎn)規(guī)則的預(yù)處理過程及其證明。對(duì)于化簡(jiǎn)后的范式，所有子句都包含至少兩個(gè)字符，同時(shí)明確了包含兩個(gè)字符的子句和其

4、他類型子句的關(guān)系，并且任意兩個(gè)不同的字符都不可能同時(shí)包含在兩個(gè)子句中。本文采用分支搜索技術(shù)對(duì)可滿足性問題進(jìn)行求解。算法在每次分支之前，對(duì)范式進(jìn)行預(yù)處理。當(dāng)預(yù)處理后的范式中含有特定的3種子句結(jié)構(gòu)之一時(shí)，算法針對(duì)這種子句結(jié)構(gòu)進(jìn)行特殊分支。否則，算法將選出范式中頻率最大的變量進(jìn)行分支。本文的主要貢獻(xiàn)除了改進(jìn)可滿足性問題算法時(shí)間復(fù)雜度外，還引入了一種全新的分析方法，即加權(quán)分治(MeasureandConquer)。該方法給范式中每個(gè)變量賦予一個(gè)