SAT是适定性(Satisfiability)问题的简称。一般形式为k-适定性问题，简称 k-SAT。而当$k>2$时该问题为NP完全的，所以我们只研究$k=2$时情况。
定义
2-SAT，简单的说就是给出$n$个集合，每个集合有两个元素，已知若干个$langle a, b angle$，表示$a$与$b$矛盾(其中$a$与$b$属于不同的集合)。从每个集合选择一个元素，使得选出的$n$个元素两两不矛盾的问题，就是2-SAT问题。显然可能有多种选择方案，一般题中只需要求出一种即可。
解决方法
我们考虑将2-SAT问题往图论的方向靠，每个元素用结点来表示，元素间的矛盾关系建边来表示。
设${a, a'}$是一个集合里的元素，${b, b'}$是另一个集合里的元素，假如$a,b$之间有矛盾，那么连边$a o b'$，表示选了$a$就要选$b'$，连边$b o a'$，表示选了$b$就要选$a'$。
这样问题就转化为了从$2 imes n$个结点里选出$n$个分属不同集合的结点，并且对于每个选出的结点，其所有后继结点也都要被选出。
方法1：dfs暴搜
就是沿着图上一条路径，如果一个点被选择了，那么这条路径以后的点都将被选择，那么，出现不可行的情况就是，存在一个集合中两者都被选择了。最坏时间复杂度为$O(nm)$，虽然后面讲的Tarjan scc缩点方法时间复杂度更优，但其求的是任意方案，若是要求字典序最小的方案，还是要用这种dfs暴搜。
例题(求字典序最小方案)：HDU-1814 Peaceful Commission
#include <cstdio> #include <cstring> const int N = 20000, M = 50000; struct Edge { int to, nex; } edge[M]; int head[N], sta[N], top, e_num; bool vis[N]; void init() { memset(head, 0, sizeof(head)); memset(vis, false, sizeof(vis)); top = e_num = 0; } void add_edge(int x, int y) { edge[++e_num].to = y; edge[e_num].nex = head[x]; head[x] = e_num; } bool dfs(int u) { if (vis[u^1]) return false; if (vis[u]) return true; vis[u] = true; sta[top++] = u; for (int i = head[u]; i; i = edge[i].nex) { if (!dfs(edge[i].to)) return false; } return true; } bool solve(int n) { for (int i = 0; i < 2 * n; i += 2) { if (!vis[i] && !vis[i^1]) { top = 0; if (!dfs(i)) { while (top) vis[sta[--top]] = false; if (!dfs(i^1)) return false; } } } return true; } int main() { int n, m; while (~scanf("%d %d", &n, &m)) { init(); for (int i = 0, u, v; i < m; i++) { scanf("%d %d", &u, &v); --u, --v; add_edge(u, v ^ 1); add_edge(v, u ^ 1); } if (solve(n)) { for (int i = 0; i < 2 * n; i += 2) { printf("%d ", vis[i] ? i + 1 : i + 2); } } else puts("NIE"); } return 0; }
方法2：Tarjan scc(强连通分量)缩点
建图后，跑一遍Tarjan SCC判断是否有一个集合中的两个元素在同一个SCC中，若有则无解，否则说明有可行方案。
下面这篇论文给出了求可行方案的方法并证明了这个算法的正确性：
这篇论文最后一步证明似乎有问题，我按个人理解修改如下：
(2) $p,q$先后被染成蓝色
不妨假设$q$后被染色，并且在把$r$染成红色的时候，......
..............................................................
如果$q$和$r$是间接矛盾的，即存在$G(x)in G''(r), G(lnot x)in G''(r')$，且$q$是$r'$的后代。又由$G$的对称性结构可知$p$必然是$r$的祖先，而$p$已经被染成了蓝色，$r$作为$p$的后代也会被染成蓝色，这与$r$被染成红色矛盾。
论文中给出的求可行方案的方法模拟起来比较复杂，下面这篇2003年国家集训队论文给出了更简便的方法，但只有PPT形式的文档，里面没有给出正确性证明：
论文中第21页PPT指出了用拓扑排序实现自底向上的顺序(即反拓扑序)后，按顺序选择和删除即可，即对于一个集合${a,a'}$，$a$通过scc缩点后属于$S$，$a'$属于$S'$，若$S$的反拓扑序小于$S'$，则选择$a$，否则选择$a'$。(注：此方法对于非对称图也适用)
由于Tarjan缩点重标号是从叶子节点往上，所以Tarjan求得的scc编号也就相当于反拓扑序，这让我们可以十分方便地求出一个可行方案，时间复杂度$O(n+m)$。
例题1(求任意方案)：传送门
例题2(判断是否可行)：
#include <iostream> #include <cstdio> #include <cstring> using std::min; const int N = 2010, M = N * N; struct Edge { int to, nex; } edge[M]; int num_e; int head[N]; int dfn[N], low[N], scc[N], sz[N], idx, tot; bool insta[N]; int sta[N], top; void init() { num_e = 0, top = 0, idx = 0, tot = 0; memset(head, 0, sizeof(head)); memset(insta, 0, sizeof(insta)); memset(scc, 0, sizeof(scc)); memset(dfn, 0, sizeof(dfn)); } void add_edge(int x, int y) { edge[++num_e].to = y; edge[num_e].nex = head[x]; head[x] = num_e; } void tarjan(int u) { dfn[u] = low[u] = ++idx; sta[++top] = u; insta[u] = true; for (int i = head[u]; i; i = edge[i].nex) { int v = edge[i].to; if (!dfn[v]) { tarjan(v); low[u] = min(low[u], low[v]); } else if (insta[v]) low[u] = min(low[u], dfn[v]); } if (dfn[u] == low[u]) { ++tot; do { scc[sta[top]] = tot; sz[tot]++; insta[sta[top]] = false; } while (sta[top--] != u); } } int main() { int n, m; while (~scanf("%d %d", &n, &m)) { init(); for (int i = 0, a1, a2, c1, c2; i < m; i++) { scanf("%d %d %d %d", &a1, &a2, &c1, &c2); add_edge(2 * a1 + c1, 2 * a2 + 1 - c2); add_edge(2 * a2 + c2, 2 * a1 + 1 - c1); } for (int i = 0; i < 2 * n; i++) { if (!dfn[i]) tarjan(i); } bool ans = true; for (int i = 0; i < 2 * n; i += 2) { if (scc[i] == scc[i+1]) { ans = false; break; } } printf("%s ", ans ? "YES" : "NO"); } return 0; }
注：Korasaju算法同样可以求scc，这里改Tarjan为Korasaju也可以，求出来的scc编号为原图缩点后的拓扑排序，而Tarjan求出来的是反拓扑序，注意其区别。