← 返回首頁
2-SAT 二元可滿足性問題
預設範例：
基本範例 (3 變數, 4 子句)
不可滿足 (矛盾)
課程排程 (4 門課)
圖 2-著色 (5 節點)
載入
求解
重置
新增子句：(
+
x
∨
+
x
)
加入
變數數量：
目前子句：
蘊含圖 (Implication Graph) & SCC 分析
求解結果
演算法說明
2-SAT (2-Satisfiability)
判斷一組由二元子句組成的布林公式是否可滿足。
每個子句 (a ∨ b) 轉化為兩條蘊含邊：¬a → b, ¬b → a
使用
Tarjan 演算法
找強連通分量 (SCC)
若 x
i
和 ¬x
i
在同一個 SCC 中 → 矛盾，無解
否則根據 SCC 拓撲序決定賦值：SCC 編號較大的文字為真
時間複雜度：O(n + m)，n = 變數數，m = 子句數