Abstract
本文包括個部份，在第一部份裡，提出了一個以矩陣相乘為基礎的解析計算方法。我們發現如果將輸入的子句集合作些前諯處理，把這些子句轉換成圖形上的點與有方向性的邊，這樣一來解析原理可用矩陣相乘的方法來施行。雖然可滿足性問題是個所謂的NP-complete 的問題，也就是說在最壞的情況下，任何計算方法都要花非常長的時間才能求得其解，但是有一些特殊的情況是很容易的。其中最重要的就是Horn可滿足性問題，這問題目前的計算方法可以在線性的時間內求得其解，它的時間複雜度是Ｏ（K ），K 是輸入子句集合的大小，另一方面，這問題已被證明是所謂的Log Space Complete問題，也就是說即使在平行處理的情況下也不可能非常快的求得其解，本文的第二部份就針對這問題提出一個平行計算方法使得這問題時間複雜度降為Ｏ（K ），K 是布林變數的數目。對於每一組子句集合，我們發現都可以找到它的子集，使得這兩個集合的可滿足性是相同的。對於這樣的子集我們提出了一個時間複雜度是Ｏ（log N ）的計算方法。最後我們指，出對這樣的問題，必需在時間與空間之間作取捨，由於這間題的特性（Log Space Complete）使得我們無法兼顧。