2-SAT¶
SAT (Булын гүйцэтгэх боломжийн бодлого) гэдэг нь өгөгдсөн Булын томьёог хангахын тулд хувьсагчдад Булын утга оноох бодлого юм. Булын томьёог ихэвчлэн CNF (конъюнктив нормаль хэлбэр)-ээр өгнө, энэ нь олон дизъюнктийн конъюнкц бөгөөд дизъюнкт бүр нь литералуудын (хувьсагч эсвэл хувьсагчийн үгүйсгэл) дизъюнкц юм. 2-SAT (2-гүйцэтгэх боломж) нь SAT бодлогын хязгаарлагдмал хувилбар бөгөөд 2-SAT-д дизъюнкт бүр яг хоёр литералтай байна. Ийм 2-SAT бодлогын жишээ энд байна. Дараах томьёо үнэн байхаар $a, b, c$-ийн оноолтыг ол:
SAT нь NP-бүрэн бөгөөд түүнд мэдэгдэж буй үр ашигтай шийд байхгүй. Гэвч 2SAT-г $O(n + m)$-д үр ашигтай бодож болно, энд $n$ нь хувьсагчийн тоо, $m$ нь дизъюнктийн тоо юм.
Алгоритм:¶
Эхлээд бид бодлогыг өөр хэлбэр буюу импликатив нормаль хэлбэр гэж нэрлэгддэг хэлбэр рүү хөрвүүлэх хэрэгтэй. $a \lor b$ илэрхийлэл нь $\lnot a \Rightarrow b \land \lnot b \Rightarrow a$-тай эквивалент болохыг анзаар (хэрэв хоёр хувьсагчийн нэг нь худал бол нөгөө нь заавал үнэн байх ёстой).
Одоо бид эдгээр импликацийн чиглэлтэй графыг байгуулна: хувьсагч $x$ бүрийн хувьд $v_x$ ба $v_{\lnot x}$ гэсэн хоёр орой байна. Ирмэгүүд нь импликацуудад харгалзана.
2-CNF хэлбэр дэх жишээг харцгаая:
Чиглэлтэй граф дараах орой ба ирмэгүүдийг агуулна:
Импликацийн графыг дараах зурагт харж болно:
Импликацийн графын дараах шинж чанарт анхаарал хандуулах нь зүйтэй: хэрэв ирмэг $a \Rightarrow b$ байвал ирмэг $\lnot b \Rightarrow \lnot a$ ч бас байна.
Мөн хэрэв $\lnot x$-ээс $x$ хүрч болох ба $x$-ээс $\lnot x$ хүрч болох бол бодлого шийдгүй гэдгийг анзаар. Бид хувьсагч $x$-д ямар ч утга сонгосон энэ нь үргэлж зөрчилд хүргэнэ — хэрэв $x$-д $\text{true}$ оноогдвол импликац бидэнд $\lnot x$ ч мөн $\text{true}$ байх ёстойг хэлэх ба эсрэгээрээ. Энэ нөхцөл нь зөвхөн зайлшгүй төдийгүй бас хүрэлцээтэй болох нь тогтоогддог. Бид үүнийг доорх хэдэн догол мөрөнд батална. Эхлээд нэг орой хоёр дахиас хүрч болох ба хоёр дахь нь эхнийхээс хүрч болох бол эдгээр хоёр орой нэг хүчтэй холбоост компонентод байна гэдгийг сана. Тиймээс бид шийд оршин байх шалгуурыг дараах байдлаар томьёолж болно:
Энэ 2-SAT бодлого шийдтэй байхын тулд дурын хувьсагч $x$-ийн хувьд орой $x$ ба $\lnot x$ нь импликацийн графын хүчтэй холбоосын өөр өөр хүчтэй холбоост компонентод байх нь зайлшгүй бөгөөд хүрэлцээтэй.
Энэ шалгуурыг бүх хүчтэй холбоост компонентыг олох замаар $O(n + m)$ хугацаанд шалгаж болно.
Дараах зураг жишээний бүх хүчтэй холбоост компонентыг харуулж байна. Бидний амархан шалгаж болохоор дөрвөн компонентын аль нь ч орой $x$ ба түүний үгүйсгэл $\lnot x$-г хамт агуулаагүй тул жишээ шийдтэй. Бид зөв оноолтыг хэрхэн тооцоолохыг дараагийн догол мөрүүдэд үзэх боловч ердөө үзүүлэх зорилгоор $a = \text{false}$, $b = \text{false}$, $c = \text{false}$ шийдийг өглөө.
Одоо бид шийд оршин байна гэсэн таамаглал дор 2-SAT бодлогын шийдийг олох алгоритмыг байгуулна.
Шийд оршин байгаа хэдий ч импликацийн графт $x$-ээс $\lnot x$ хүрч болох, эсвэл (гэхдээ нэгэн зэрэг биш) $\lnot x$-ээс $x$ хүрч болох тохиолдол гарч болохыг анзаар. Тэр тохиолдолд $x$-д $\text{true}$ эсвэл $\text{false}$-ийн аль нэгийг сонгох нь зөрчилд хүргэх ба нөгөөг нь сонгох нь хүргэхгүй. Зөрчил үүсгэхгүй байхаар утгыг хэрхэн сонгохыг сурцгаая.
Хүчтэй холбоост компонентуудыг топологийн эрэмбээр эрэмбэлье (өөрөөр хэлбэл $v$-ээс $u$ хүрэх зам байвал $\text{comp}[v] \le \text{comp}[u]$) ба $\text{comp}[v]$ нь орой $v$ харьяалагдах хүчтэй холбоост компонентын индексийг тэмдэглэе. Тэгвэл хэрэв $\text{comp}[x] < \text{comp}[\lnot x]$ бол бид $x$-д $\text{false}$, эс бөгөөс $\text{true}$ ононо.
Хувьсагчдын энэ оноолтоор бид зөрчилд хүрэхгүй гэдгийг батлая. $x$-д $\text{true}$ оноогдсон гэж үзье. Нөгөө тохиолдлыг ижил төстэй аргаар батлаж болно.
Эхлээд орой $x$ нь орой $\lnot x$ хүрч чадахгүйг батлая. Бид $\text{true}$ оноосон тул $x$-ийн хүчтэй холбоост компонентын индекс $\lnot x$-ийн компонентын индексээс их байх ёстой. Энэ нь $\lnot x$ нь $x$-г агуулсан компонентын зүүн талд байрлана гэсэн үг бөгөөд хожуу орой эхнийхэд хүрч чадахгүй.
Хоёрдугаарт импликацийн графт орой $y$ ба $\lnot y$ хоёул $x$-ээс хүрч болохоор хувьсагч $y$ оршихгүйг батлая. Энэ нь зөрчил үүсгэх байсан, учир нь $x = \text{true}$ нь $y = \text{true}$ ба $\lnot y = \text{true}$-г илэрхийлнэ. Үүнийг зөрчлөөр батлая. $y$ ба $\lnot y$ хоёул $x$-ээс хүрч болно гэж үзвэл импликацийн графын шинж чанараар $\lnot x$ нь $y$ ба $\lnot y$ хоёулангаас хүрч болно. Транзитив чанараар энэ нь $\lnot x$-д $x$-ээс хүрч болно гэсэн үр дүнд хүрэх ба энэ нь таамаглалтай зөрчилдөнө.
Ингэснээр бид дурын хувьсагч $x$-ийн хувьд орой $x$ ба $\lnot x$ өөр өөр хүчтэй холбоост компонентод байна гэсэн таамаглал дор хувьсагчдын шаардлагатай утгыг олох алгоритмыг байгуулсан. Дээр энэ алгоритмын зөв байдлыг харуулсан. Улмаар бид шийд оршин байх дээрх шалгуурыг нэгэн зэрэг баталсан.
Implementation:¶
Now we can implement the entire algorithm. First we construct the graph of implications and find all strongly connected components. This can be accomplished with Kosaraju's algorithm in $O(n + m)$ time. In the second traversal of the graph Kosaraju's algorithm visits the strongly connected components in topological order, therefore it is easy to compute $\text{comp}[v]$ for each vertex $v$.
Afterwards we can choose the assignment of $x$ by comparing $\text{comp}[x]$ and $\text{comp}[\lnot x]$. If $\text{comp}[x] = \text{comp}[\lnot x]$ we return $\text{false}$ to indicate that there doesn't exist a valid assignment that satisfies the 2-SAT problem.
Below is the implementation of the solution of the 2-SAT problem for the already constructed graph of implication $adj$ and the transpose graph $adj^{\intercal}$ (in which the direction of each edge is reversed). In the graph the vertices with indices $2k$ and $2k+1$ are the two vertices corresponding to variable $k$ with $2k+1$ corresponding to the negated variable.
struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;
TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) {
order.reserve(n_vertices);
}
void dfs1(int v) {
used[v] = true;
for (int u : adj[v]) {
if (!used[u])
dfs1(u);
}
order.push_back(v);
}
void dfs2(int v, int cl) {
comp[v] = cl;
for (int u : adj_t[v]) {
if (comp[u] == -1)
dfs2(u, cl);
}
}
bool solve_2SAT() {
order.clear();
used.assign(n_vertices, false);
for (int i = 0; i < n_vertices; ++i) {
if (!used[i])
dfs1(i);
}
comp.assign(n_vertices, -1);
for (int i = 0, j = 0; i < n_vertices; ++i) {
int v = order[n_vertices - i - 1];
if (comp[v] == -1)
dfs2(v, j++);
}
assignment.assign(n_vars, false);
for (int i = 0; i < n_vertices; i += 2) {
if (comp[i] == comp[i + 1])
return false;
assignment[i / 2] = comp[i] > comp[i + 1];
}
return true;
}
void add_disjunction(int a, bool na, int b, bool nb) {
// na and nb signify whether a and b are to be negated
a = 2 * a ^ na;
b = 2 * b ^ nb;
int neg_a = a ^ 1;
int neg_b = b ^ 1;
adj[neg_a].push_back(b);
adj[neg_b].push_back(a);
adj_t[b].push_back(neg_a);
adj_t[a].push_back(neg_b);
}
static void example_usage() {
TwoSatSolver solver(3); // a, b, c
solver.add_disjunction(0, false, 1, true); // a v not b
solver.add_disjunction(0, true, 1, true); // not a v not b
solver.add_disjunction(1, false, 2, false); // b v c
solver.add_disjunction(0, false, 0, false); // a v a
assert(solver.solve_2SAT() == true);
auto expected = vector<bool>(True, False, True);
assert(solver.assignment == expected);
}
};