2-SAT
2-SAT
設 $n$ 個布爾變量 $f_1, f_2, ..., f_n$ .
給定 $m$ 個形如 " 變量 - 邏輯運算符 - 變量 " 的二元限制條件, 例如 $f_1 ~ and ~ f_2$ .
解布爾變量.
就現在的研究層次, 我們要解決的問題是 存在性 層次的相關問題:
① 解什麽時候存在.
② 構造一組合法解.
③ 構造一組字典序最小的解.
等價建圖
我們將每個布爾變量 $f_x$ , 拆成兩個點 $x, x‘$ , $x$ 代表 true , $x‘$ 代表 false .
我們定義蘊含關系:
如果選擇了點 $x$ , 那麽必須選擇點 $y$ .
對應地, 我們在圖中連邊 $x \rightarrow y$ .
蘊含關系具有傳遞性.
舉個例子: $f_x ~ or ~ f_y$ 應該如何連邊?
若 $f_x$ 為假, 則 $f_y$ 必然為真. ---- ①
逆否命題: 若 $f_y$ 為假, 則 $f_x$ 必然為真. ---- ②
我們發現 ①② 不僅是必要條件, 同時也是充分條件, 即 $f_x ~ or ~ f_y \Leftrightarrow ①②$ .
所以我們連邊 $x‘ \rightarrow y, y‘ \rightarrow x$ .
我們不難發現, 建出來的圖是左右對稱的.
那麽, 我們現在的問題被轉化為:
① 在圖中的每個點對中選擇一個點.
② 若一個點被選擇, 則它的所有後繼都要被選擇.
問題解決
我們考慮對這張圖跑 Tarjan 算法, 求強連通分量.
並對所有的強連通分量, 按照結束訪問的時間, 從小到大進行標號.
如果存在 $x, x‘$ 在同一個強連通分量內, 那麽一定無解.
因為選擇了 $x$ 就必須要選擇 $x‘$ , 選擇了 $x‘$ 就 $x$ , 而我們目標每個點對中選擇一個.
否則, 我們可以嘗試構造性地證明一定有解.
我們如果選擇了某個強連通分量內的點, 那麽整個強連通分量都要選擇.
我們按照強連通分量, 將圖進行縮點.
現在的問題和原問題的形式是一致的:
① 現在的點是原本的強連通分量.
② 我們有 $m$ 個點對.
③ 每個點 $x$ 具有一個標號 $L_x$ .
④ 圖具有左右對稱的性質.
⑤ 我們要在每個點對中選擇一個點, 且如果一個點被選擇, 那麽它的所有後繼都要被選擇.
點的標號存在一些性質.
如果存在邊 $x \rightarrow y$ , 那麽 $L_y < L_x$ .
證明
① 當我們訪問 $x$ 的時候, 還沒有訪問到 $y$ , 那麽一定會先結束訪問 $y$ .
② 當我們訪問 $x$ 的時候, 已經訪問過 $y$ , 那麽 $y$ 在 $x$ 前先結束訪問.
我們對於每個點對 $(x, y)$ , 選擇標號小的點.
證明:
① 我們對每個點對 $(x, y)$ , 選擇標號小的點, 那麽已經能滿足 "每個點對中選擇一個點" 的約束條件.
② 證明 "如果一個點被選擇, 那麽它的所有後繼都要被選擇." .
假設原圖中存在點 $x$ , 它有後繼 $y$ , 我們選擇了點 $x$ , 卻沒有選擇點 $y$ .
那麽有
$$\begin{aligned} L_y & > L_{y‘} & (選擇了 y‘ 卻沒有選擇 y) \\ & > L_{x‘} & (圖的對稱性 + 標號性質) \\ & > L_x & (選擇了 x 卻沒有選擇 x‘) \\ & > L_y & (標號性質) \end{aligned}$$
所以矛盾, 所以必然不存在這種情況.
總結一些, 我們得到了兩個重要的結論:
① 2-SAT 問題有解, 當且僅當不存在 $x$, $x‘$ , $x$ 和 $x‘$ 在同一個強連通分量內.
② 若 2-SAT 問題有解, 那麽我們對每對強連通分量, 取標號較小的, 即對每個變量 $f_x$ , 取它對應的強連通分量的標號較小的.
一元限制條件
有些問題中還增加了一元限制條件 $not ~ f_x$ , $f_x$ .
$not ~ f_x \Rightarrow (x \rightarrow x‘)$ .
$f_x \Rightarrow (x‘ \rightarrow x)$ .
我們嘗試兼容這種情況, 即嘗試對構造性證明加以補充.
若 $x \rightarrow x‘$ , 那麽必然選擇 $x‘$ .
而對於標號必有 $L_{x‘} < L_x$ , 根據構造性證明的過程, 必然選擇 $L_{x‘}$ .
二者得以統一.
2-SAT