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

1、在可計(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為真?？蓾M足性問題算法的時(shí)間復(fù)雜度計(jì)算過程主要涉及3類參數(shù):范式中變量的個(gè)數(shù)n，范式中子句的個(gè)數(shù)m，范式中字符的個(gè)數(shù)L。
　　本文從字符個(gè)數(shù)L的角度

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

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