使用蠻力解決2Sat CNF形式

我目前正在研究考試的2SAT問題，我真的不明白如何使用蠻力檢查解決方案是否存在。我知道這看起來有點奇怪，但我理解如何更好地實現蘊含圖，但我不太清楚如何實施暴力破解策略。使用蠻力解決2Sat CNF形式

任何人都可以分享一些見解嗎？也許在僞代碼或Java。

感謝

2013-02-08 John Smith

也許你錯過了2-SAT的基礎知識呢？蠻力方法只是爲所有變量生成true和false之間的所有排列，然後檢查當前排列是否滿足給定的子句集合。 – mmgp 2013-02-08 18:49:18

對不起，這個問題可能措辭不佳。我明白，蠻力方法生成所有的排列，但我覺得就像我這樣做，即使是一個暴力的實施，這是非常殘酷的。我創建了一個包含所有可能的組合的2D數組，然後檢查輸入解決方案逐行。它似乎適用於少數幾個分離，但是數組的大小很快就會失控，並且我得到一個堆空間異常。 – 2013-02-08 19:04:10

強大的連接組件很容易實現，而且效率更高，並會告訴您是否有解決方案。那有什麼問題？ – mmgp 2013-02-08 19:53:03

公式中的變量可以編碼爲整數值中的位。暴力方法然後歸結爲整體「集裝箱」可能採取的所有可能值的範圍。

換句話說，您有一個整數數組，代表所有公式的變量，並且您用整數遞增整數，並且在每一步中檢查它對您公式的解決方案。當解決方案匹配時停止。

下面是這樣一個變量容器死簡單的實現：

class OverflowException extends RuntimeException {} 

public class Variables { 
    int[] data; 
    int size; 

    public Variables(int size_){ 
     size = size_; 
     data = new int[1 + size/32]; 
    } 
    public boolean get(int i){ 
     return (data[i/32] & (1 << i%32)) != 0; 
    } 
    public void set(int i, boolean v){ 
     if (v) 
      data[i/32] |= (1 << i%32); 
     else 
      data[i/32] &= ~(1 << i%32); 
    } 
    public void increment(){ 
     int i; 
     for (i=0; i < size/32; i++){ 
      data[i]++; 
      if (data[i] != 0) return; 
     } 
     if (size%32 != 0){ 
      data[i]++; 
      if ((data[i] & ~((1 << (size%32)) - 1)) != 0) 
       throw new OverflowException(); 
     } 
    } 
}

（買者自負：未測試的代碼）。

的數組變量也可以更簡單地表示爲boolean容器，但你可能在性能上損失一點，因爲增量步驟（雖然這可以通過使用gray code而不是爲普通的二進制編碼來或許緩解增量操作，但這個implementation的複雜性似乎表明了相反的情況，如果你想要一個複雜的解決方案，它可能是一個好的sat2求解器）。

來源

2013-02-08 20:15:18 didierc

我不太流利的Java，所以我的代碼可能沒有遵循標準做法，請告知，或編輯。 – didierc 2013-02-08 20:46:51

這是我們不要用蠻力解決方案:)的原因，他們要消耗多少資源。我的算法不是創建一個具有所有可能性的矩陣。但要創建一個作業，然後立即進行測試。然後創建下一個。當你找到第一個解決方案時，你可以停下來。

來源

2013-02-08 19:16:40 dolbi

目前，我只是想看看2SAT是否有解決方案。發現所有可能性需要太多：D – 2013-02-08 19:18:42

正如我所提到的，您可以停止第一次正面作業的運行。這樣你就不需要爲所有作業分配空間，只需檢查它們並停止。 – dolbi 2013-02-08 19:21:32

@dolbi我不確定你是否在開玩笑，但這個解決方案和任何暴力破解一樣糟糕（無論他們是否試圖一次存儲所有的排列）。生成一個接一個的排列不會節省任何計算時間，但在最壞的情況下它仍然是'O（n！）'。立即產生所有排列是毫無意義的，甚至不應該被考慮。 – mmgp 2013-02-08 19:57:09

使用蠻力解決2Sat CNF形式

回答

相關問題