Abstract
所謂滿足性問題(Satisfiability Problem)就是指對於一組任意給定的布林函數F,決定其是否存在一組或一組以上之 "給定真值(Truth Value Assignment)" 使得此布林函數F 為真o 如果在滿足性問題上再加上一個條件 "布林函數中每一個子句(Clause)的精確子(Literals)個數均為K"則稱此類滿足性問題為 K- 滿足性問題(k-Satisfia-bility Problem)o滿足性問題和K-滿足性問題, K≧3, 均已被證明是" 非決定性多項完整問題(NP-Complete Problem)"o 雖然如此, 我們還是可以看到很多計算方法不斷地被證明其平均狀況為多項函數時間(Polynomial Time)o在人工智慧研究的課題上, 我們稱解決滿足性問題為自動定理證明o 目前已有很多自動定理證明之計算方法被提出。在這些已發明的自動定理證明之計算方法中, 有一些是根據回朔技巧(Branching Techniques), 有些則是建立在Davis 和Putnam所提出的方法上。另外, 還有一些是採用解析原理來解滿足性問題。由於到目前為止, 我們尚無法找到更好的計算方法能在最差的情況下, 用多項函數時間解決像滿足性問題這類的非決定性多項完整問題。因此, 在過去的研究中, 有不少論文轉而研究計算方法之行為模式。就滿足性問題和K-滿足性問題來說, 大部份論文致力於Davis-Putnam方法之不同版本在平均狀況下之分析研究。在此博士論文中, 我們提出了一個解析原理計算方法的平均狀況分析與研究。在上述各計算方法之平均狀況分析論文中, 有些計算方法擁有在多項函數時間的平均表現。但有些在某機率分布下, 卻是指數函數的平均表現(Exponential Time Behav-ior)。在本博士論文中, 我們將相關研究作了簡單的回顧, 以便了解自動定理證明方法在過去的研究中所得到的結果, 並藉以比較本論文中之研究成果。並對於兩個自動定理證明方法作平均狀況之分析與研究。在這兩個方法, 一個是利用解析原理(ResolutionPrinciple)來解滿足性問題, 另一個則是利用分歧技巧(Branching Techniques)來回答K-滿足性問題之答案。對於利用解析原理的計算方法, 我們得到當P。 被視為常數, 而且r。 定為n 的多項函數時, 其平均被處理子句之期望總數為O(n+r。), 其中n為變數的個數,r。是原輸入時之子句個數,P。是原始給定之變數出現在子句中為正或為負的機率。另外, 對於利用分歧技巧之計算方法, 我們拿它來解K-滿足性問題, 並證明當lim ∞,n 很大, 以及K 是常數時, 其平均執行時間為指數函數時間(Expo-nential Time),其中是r 是原輸入之子句個數, 而且每個子句都是從所有在n 個變數下可能的K-精確子(K-literal) 子句之集合中隨機獨立選取的。