問題が多項式時間で解ける場合、Digraph に強結合コンポーネントを適用すると、 2-SAT ブール値の充足可能性を確認できることがわかっています。
問題が充足可能であると仮定しましょう。
質問: 2-SAT に依存してその解を計算するための一般的なアルゴリズムはありますか?
問題が多項式時間で解ける場合、Digraph に強結合コンポーネントを適用すると、 2-SAT ブール値の充足可能性を確認できることがわかっています。
問題が充足可能であると仮定しましょう。
質問: 2-SAT に依存してその解を計算するための一般的なアルゴリズムはありますか?
私があなたの質問を正しく理解していると仮定すると、はい、充足可能性問題のアルゴリズムを使用して解 (つまり、満足のいく割り当て) を見つけるための一般的なアルゴリズムがあります。
元の値から新しい 2-CNF を作成するために、変数 x iに値「true」を割り当てるとします (リテラル x iが true で ~x iが false になるように)。充足可能性を実行する場合 (つまり、SCC を使用して、新しい CNF が充足可能かどうかを確認します):
アルゴリズムの背後にあるアイデアは、ケース 1 にヒットした場合は変数を「false」にし、ケース 2 にヒットした場合は「true」にして、すべての変数をループすることです (既に見た変数に行った割り当てを保持します)。 . 私が提起した質問に答えることができれば、その背後にある概念を理解できます。