SAT 是适定性（Satisfiability）问题的简称。一般形式为 k - 适定性问题，简称 k-SAT。而当 \(k>2\) 时该问题为 NP 完全的。所以我们只研究 \(k=2\) 的情况。
而 2-SAT 问题一般指的是，有 \(n\) 个布尔变量 \(x_1,x_2\dots x_n\)，现在有若干个二元的运算，是对于 \(x_i,\neg x_i,x_j \neg x_j\) 进行 \(\land,\lor\) 或 \(\oplus\)，运算，问是否存在一种分配方式，使得所有的这些运算均为真。
因为它是二元的，所以叫做 2-SAT。
解决这个问题的关键就是将所有的逻辑语句统一，统一成 \(p\to q\) 的形式。即 “如果选择了 \(p\)，就必须选 \(q\)”。
这样，我们将所有的 \(p\to q\) 看作有向边，我们可以得到一张有向图。
那么我们可以知道，在同一个强连通分量中的所有点，要么同时选择，要么同时不选择。我们跑 Tarjan 缩强连通分量之后，会得到一个 DAG。
这是无解的条件就很明显：如果存在 \(x_i\) 和 \(\neg x_i\) 在同一个强连通分量之中，则说明无解。然后我们对整张图进行缩成的 DAG 进行拓扑排序，每一个变量选择拓扑序较大的决策即可。
Luogu P4782 【模板】2-SAT 问题
有 \(n\) 个布尔变量，有 \(m\) 条件为 \(x_i\) 为真/假或 \(x_j\) 为真/假。询问是否有合法解，并给出一组构造。
每一个操作形如 \(a\lor b\)，相当于 \(\neg a\to b\land \neg b\to a\)，建图即可。
[JSOI2010] 满汉全席
有 \(n\) 种食材，每种食材要做成两种食品中的一个，有 \(m\) 个要求，每一个形如至少要有两种食品中的一个，问是否可以满足所有要求。
和上面一道题形式几乎相同。
[HNOI2010] 平面图判定
给定一张图，并给出他的一个哈密顿回路，判断这张图是否可以变成平面图。
根据平面图的定理，可以得到平面图的边数至多为 \(3n+6\) 条，那么对于每一个不在哈密顿回路上的边，它要么在环外，要么在环内。
对于每一对边，暴力判断他们同时在环外或环内是否会有交，如果有，则他们之间会出现 \(x_i\oplus x_j=1\) 的限制，拆成 \(x_i\leftrightarrow \neg x_j\)，\(\neg x_i\leftrightarrow x_j\) 即可。
由于这个限制是双向的，可以直接使用并查集维护。
[北京省选集训2019] 完美塔防
不难证明，每一个 . 至多只会被两束合法的激光覆盖，具体的，因为没有任何可以使光线回合的一起，每一个方向至多只会有一条激光，而如果相对的方向都有激光则说明这样的组合是不合法的，因为他们会打到另一个仪器。
所以直接暴搜查询每一个点是否会被哪些光遍历，以及哪些光是合法的这样的操作复杂度是正确的，然后对于每一个位置，都是 \(a\) 或 \(b\) 的信息，直接见图跑 2-SAT 即可。
[NEERC2016] Binary Code
有 \(n\) 个 \(01\) 串，每个串至多有一个位置是不确定的，问是否有一种确定每一个不确定位的方式，使得没有任何一个串是另一个串的前缀。
由于每一个串至多有一个不确定位，相当于是在两种可能中选择，暴力连接所有可能的前后缀是 \(O(n^2)\) 量级的边数，显然无法接受，所有考虑优化建边的过程。
具体的，我们考虑建出Trie树，这样每一个点的前后缀关系都可以在树上轻松表示出来，建两颗辅助的Trie树，一个向叶，一个向心即可，边数是 \(O(\sum |S|)\) 的，再跑 2-SAT 即可。