您好，歡迎來電子發(fā)燒友網(wǎng)！ ，新用戶？[免費注冊]

您的位置：電子發(fā)燒友網(wǎng)>源碼下載>數(shù)值算法/人工智能>

聚類和劃分的SAT分治判定

大?。?/span>0.58 MB 人氣： 2018-01-24 需要積分：2

推薦 + 挑錯 + 收藏(0) + 用戶評論（0）

前往下載地址

　 提出了一種將布爾公式劃分為子句組來進行布爾可滿足性判定的方法．CNF（conjunctive normal form）公式是可滿足的當(dāng)且僅當(dāng)劃分產(chǎn)生的每個子句組都是可滿足的。因此，通過判定子句組的可滿足性來判定原公式的可滿足性，相當(dāng)于用分治法將復(fù)雜問題分解為多個子問題來求解．這種分治判定方法一方面降低了原公式的可滿足性判定復(fù)雜度；另一方面，由于子句組的判定可以并行，因而判定速度能夠得到進一步的提高．對于不能直接產(chǎn)生布爾子句組劃分的情形，提出了一種利用聚類技術(shù)將CNF公式聚類成多個簇，然后消去簇間的公共變量來產(chǎn)生子句組劃分的方法．

非常好我支持^.^

(0) 0%

不好我反對

(0) 0%

      發(fā)表評論

      用戶評論
      評價:好評中評差評

      發(fā)表評論，獲取積分！ 請遵守相關(guān)規(guī)定！

      ?