2017-04-02 80 views
1

我正在解決SCCs的兩個可滿足性問題,並且有關於拓撲排序的問題。我基於此的算法是以逆向拓撲順序處理SCC,這在所有連接時都很好。我的算法是打破的情況下是這樣的:2可滿足性強連接組件拓撲排序

3 3 
-2 3 
1 -2 
-2 -1 

這使得看起來像這樣的圖表: Graph of problem

有兩個來源,並在此圖中,兩個水槽,並根據你開始有多個拓撲排序,所以有兩個可能的最終節點。沒有周期,所以每個節點都是SCC。從源到匯有多條路徑,所以當我做逆向拓撲順序時,我可以從接收器x3開始或接收器!x2。給我一個正確答案的路徑是從!x2開始,這將導致1,-2,-3或-1,-2,-3,這兩個都是解。但是如果我從x3開始,一個可能的結果是-1,2,3,這不是一個解決方案。

所以當我看着我的兩個水槽時,我該如何決定最後的拓撲?很明顯,答案是!x2,但我試圖弄清算法將如何確定這一點。我看到四個可能的思路:

  • X2是最後的,因爲它有更多的節點通往它
  • X2是最後一個,因爲它是在一個較長的路徑
  • 結束設置每個真值!在我開始處理任何東西之前,接收器的數量是
  • 沒有辦法知道哪個是最後一個,因此創建所有可能的解決方案並測試它們中的每一個以查看它是否有效。

還是有什麼關於拓撲順序SCCs我不在這裏?這是基於我在之前的課程中通過強連通組件賦值的算法,因此它不會完全錯誤。

回答

1

沒有看到你的代碼,我不能確定,但​​我的猜測是,當你處理文字時,你將設置一個值,然後當你在拓撲順序中遇到它的否定時,再翻轉它。關鍵是,一旦你設置了一個變量,你不會再改變它。跳過已具有設定值的任何變量的字面值。

編輯添加:從您的評論我認爲我看到了問題。當!x2在逆拓撲排序中首先出現時,您提到將變量x2設置爲true。您應該將文字!x2設置爲true,這表示您將變量 x2設置爲false。如果你這樣做,那麼你的求解器應該工作,不管你開始使用哪個接收器。

+0

感謝您的回覆。我沒有包含我的代碼,因爲它很長,這更多的是一個理論問題,但我不是在翻動數字。我正在跳過已經設置的任何東西。算法所做的是過程x3 true和!x3 false,然後x2 true和!x2 false。然後它從另一個sink,!x2開始,但在跳過之前它已經被設置爲false,然後回退到!x1並設置爲true,x1爲false,然後停止,結果爲-1 2 3.所以你可以通過遵循你所描述的規則來看待我被導致錯誤的答案。 – jimboweb

+0

@jimboweb根據新信息編輯答案,希望它有幫助。 –