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

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

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

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

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