如何獲得2-Sat值

Question

每當我搜索2-Sat算法時，我都會回到問題決策形式的算法：是否存在一組符合所有子句的合法值。但是，這不允許我輕鬆找到一組令人滿意的布爾值。

如何有效地找到一組符合2-Sat實例的合法值？

我在C++中使用boost庫，希望能夠很容易地集成代碼。

在此先感謝

Answer 1

如果你有，如果存在有效的檢測判定算法分配到2-SAT，你可以使用它來真正找出實際的任務。

首先對整個表達式運行2-SAT決策算法。假設它說有一個有效的任務。

現在，如果X_1是文字，分配X_1爲0。現在，計算2-SAT爲結果表達式（你將不得不分配，因爲這一些其他的文字，例如，如果出現X_1 OR X_3，你也需要將x_3設置爲1）。

如果得到expresion是2-滿足的，那麼你可以採取X_1爲0，否則採取X_1爲1

現在，你可以發現這一點對每個文字。

對於更高效的算法，我建議你嘗試使用蘊涵圖方法。

您可以在這裏找到更多的信息：http://en.wikipedia.org/wiki/2-satisfiability

相關部分：

2可滿足實例 解當且僅當該實例的每個變量 屬於不同的 強烈 蘊含圖的連通分量比否定 相同的變量。由於通過基於 深度優先搜索的算法可以在 線性時間中發現強連接分量，所以相同的線性時間限制也適用於 2-可滿足性。

在每個強連通分量的文字或者是全零或全1

Answer 2

有至少一個算法，列出了所有的解決方案，以一個2-SAT問題，由托馬斯·費德：http://www.springerlink.com/content/j582276p06276l12/