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

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

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

3、都不可能同時包含在兩個子句中。
　　本文采用分支搜索技術(shù)對可滿足性問題進行求解。算法在每次分支之前，對范式進行預處理。當預處理后的范式中含有特定的3種子句結(jié)構(gòu)之一時，算法針對這種子句結(jié)構(gòu)進行特殊分支。否則，算法將選出范式中頻率最大的變量進行分支。本文的主要貢獻除了改進可滿足性問題算法時間復雜度外，還引入了一種全新的分析方法，即加權(quán)分治(Measure and Conquer)。該方法給范式中每個變量賦予一個權(quán)值，該權(quán)值在分支過程中