2-satisfiability

1熱度

1回答

我有一個問題，它是2-SAT問題的延伸。在標準的2-SAT問題中，我們可以找到任何取決於我們選擇的頂點排序的真值分配。我想檢查是否存在唯一的表達式可滿足的真值賦值（即只有一個組合）。文字的數量可以是100000. 一種方法是找到所有可能的真值賦值，然後將它們進行比較，如果它們是不同的。但問題是每次比較，我將不得不比較100000個值（沒有文字）。有沒有什麼有效的方法？

3熱度

2回答

2-Satisfiability問題中的實現問題

我想爲100000個文字實現2-SAT問題。所以會有20萬個頂點。所以我被困在從每個頂點有一個所有可到達頂點的數組，空間複雜度爲O(200000^2)，這是不可行的所以請爲此建議一個解決方案。請介紹一下2-SAT問題的有效實施。

0熱度

2回答

使用蠻力解決2Sat CNF形式

我目前正在研究考試的2SAT問題，我真的不明白如何使用蠻力檢查解決方案是否存在。我知道這看起來有點奇怪，但我理解如何更好地實現蘊含圖，但我不太清楚如何實施暴力破解策略。任何人都可以分享一些見解嗎？也許在僞代碼或Java。感謝

0熱度

2回答

2 SATisfiabilty問題測試用例

我已經寫了SAT求解器2可滿足性問題，有人請我提供它只有一個令人滿意的分配，即只有一個解決方案一個測試用例說10000個文字 The format can be:(for 3 literals) 2 // No of clauses and then each clause 2 3 1 -2 corresponding to (b+c).(a+!b)

1熱度

1回答

2-SAT相關算法的多項式算法

我讀了很多找到2-SAT問題的算法，即給定的表達式是可滿足與否，可以用多項式時間求解。示例（algorithm）。對於Krom的程序（Wikipedia），我構造了一個圖，從中我可以很容易地驗證它在多項式時間內的可滿足性。現在，我想找到這個表達式的解決方案是可以滿足的。我在想這個（驗證它）：首先我將任何形式的強連通分量表達式寫成x，並將值賦值爲0.然後按照算法，存在邊（x！ - > y）。因

1熱度

1回答

2可滿足性強連接組件拓撲排序

我正在解決SCCs的兩個可滿足性問題，並且有關於拓撲排序的問題。我基於此的算法是以逆向拓撲順序處理SCC，這在所有連接時都很好。我的算法是打破的情況下是這樣的： 3 3 -2 3 1 -2 -2 -1 這使得看起來像這樣的圖表：有兩個來源，並在此圖中，兩個水槽，並根據你開始有多個拓撲排序，所以有兩個可能的最終節點。沒有周期，所以每個節點都是SCC。從源到匯有多條路徑，所以當我做逆向拓撲

2熱度

1回答

蘊涵圖分配

蘊含圖是一個有向圖，其中每個節點都分配了true或false，並且任何邊都暗示着if u is true then v is true。我知道一個簡單的O(n^2)算法來找出在一般蘊涵圖的分配和O(n)算法某些特殊情況下（如從2-SAT問題產生的蘊涵圖）。所以我想知道是否有O(n)算法找到任何蘊涵圖的任務？

0熱度

1回答

如何解決一個2-SAT實例使用Z3Py

我使用下面的代碼60個布爾變量和99項條款： X = BoolVector('x', 60) M = [[21, 34],[-49, -12],[7, 18], [-5, -1],[28, 17], [3, 55],[36, 33], [-6, -50],[44, -41], [-55, 3],[14, -54],[-30, 13], [-13,

2熱度

1回答

有沒有人看過2-Sat實現

我一直在尋找一段時間，但我似乎無法找到2-Sat算法的任何實現。我在C++中使用boost庫（其中有strongly connected component module），需要一些指導來創建一個有效的2-Sat程序或找到一個現有的庫供我通過C++使用。

4熱度

2回答

如何獲得2-Sat值

每當我搜索2-Sat算法時，我都會回到問題決策形式的算法：是否存在一組符合所有子句的合法值。但是，這不允許我輕鬆找到一組令人滿意的布爾值。如何有效地找到一組符合2-Sat實例的合法值？我在C++中使用boost庫，希望能夠很容易地集成代碼。在此先感謝