2-SAT

SAT问题指的是给出一些条件（未知量经过逻辑运算的结果），问是否存在一种合法的方案使得其满足所有条件。
而2-SAT问题是一种特殊的SAT问题，它限制了每个逻辑运算的表达式中最多有两个未知量。

二元逻辑运算的转化

为了解决2-SAT问题，我们需要将所有给出的二元逻辑运算式进行转化，变成形如“若A取值为x则B取值为y”这样的条件，通常情况下，我们将取值限定在0和1。
那么对于各种逻辑运算我们就可以进行转化：

A and B = 0 —> 若A=1则B=0，若B=1则A=0
A or B = 1 —> 若A=0则B=1，若B=0则A=1
…

诸如此类，我们可以将所有的二元逻辑运算式表述成如上的形式。
特别地，如果有A=1这样的表达式，我们可以转化成“若A=0，则A=1”。

建图

那么为什么要进行这样的转化呢？因为这样的话，我们就可以将“某元素取值为x”这样的一个表述抽象成一个点，通过连边的方式来构建不同元素取值之间的关系。
具体地，根据上面的例子，我们将每个点a拆成两个点a0和a1，分别表示“a取值为0”和“a取值为1”，对于“若A=x则B=y”，我们连有向边(Ax, By)，这样的话如果我们能在图上从点P走到点Q，就说明若命题P成立则命题Q成立。
那么显然，如果能从a0走到a1且能从a1走到a0，则必然矛盾，这一步我们可以用tarjan求强连通分量解决。
反之，则一定存在合法方案满足所有的二元逻辑运算式。

求解

O(N+M)求一组可行解

首先当然是通过tarjan求强连通分量，最后如果有a0与a1在同一个强连通分量内，说明无解。
那么缩完点后，我们如何来找到一组合法的解呢？
这里先给出策略：缩点后按照逆拓扑序，即与拓扑序刚好相反的顺序找到一个未被染色的点并染成黑色，然后将与这个强连通分量中的点矛盾的所有强连通分量全部染成白色，重复这一过程，最后所有染成黑色的强连通分量里的点就是一组可行解。
那么如何证明这种策略的正确性呢？首先通过前面的缩点我们保证了强连通分量内没有矛盾，那么我们只需要证明染色的过程没有矛盾。
显然，我们在染黑色点的时候已然将其对立点所在联通块全部染成白色，染色过程不会产生矛盾，现在只需要说明我们的染色过程能够覆盖到每一个未知量。
我们假设某一个未知量的两个对应元素都被染成了白色，那么考虑我们的染色过程，某个点被染成白色必然是因为其对立点被染成了黑色，这就产生了矛盾，所以不存在同一个未知量的两个对应元素都被染成白色，所以这两个点必然是一白一黑。
如此，我们就证明了这个方法的正确性。

那么具体如何来操作呢？实际上非常方便，因为我们在缩点的过程中会对所有强连通分量进行编号，而这个编号我们从小到大来编，这样的话越靠后的强连通分量获得的编号实际上越小（因为tarjan是用dfs实现的），因此强连通分量的编号实际上就是上面提到的“逆拓扑序”。那么结果就很明显了，对于未知量a，若$ltk[a_0] < ltk[a_1]$，则$a=0$；若$ltk[a_1]<ltk[a_0]$，则$a=1$

O(NM)求最小字典序解

我们只需要枚举每一个未知量，若其取值合法就继续下去，否则取另一个值并继续下去。

关于O(NM)做法的一个优化

如果我们能在遍历到x时就能判断出x是否能走到x’，就可以O(n+m)求解了，而这个预处理我们通过传递闭包实现。

传递闭包

什么是传递闭包？一个n顶点DAG的传递闭包可以定义为一个n阶布尔矩阵$T=\{t_{i,j}\}$，若从i到j存在一条路径，则$t_\{i,j\}=1$，否则$t_{i,j}=0$。
实际上，传递闭包揭示的是两点间的传递关系，即两点间是否存在直接或间接的关系。

二分图带权匹配（KM）

最大权匹配模板

int n;
ll a[N][N], ex[N], ey[N], slack[N];
int pre[N], mat[N], vis[N], ans[N];
void bfs(int x) {
    fill(slack, slack + n + 1, INF);
    fill(pre, pre + n + 1, 0);
    fill(vis, vis + n + 1, 0);
    int y = 0, yy = 0;
    mat[0] = x;
    do {
        x = mat[y], vis[y] = 1;
        ll d = INF;
        for (int i = 1; i <= n; i++) {
            if (vis[i])
                continue;
            ll val = ex[x] + ey[i] - a[x][i];
            if (val < slack[i])
                slack[i] = val, pre[i] = y;
            if (slack[i] < d)
                d = slack[i], yy = i;
        }
        for (int i = 0; i <= n; i++)
            if (vis[i])
                ex[mat[i]] -= d, ey[i] += d;
            else
                slack[i] -= d;
        y = yy;
    } while (mat[y]);
    for (; y; y = pre[y])
        mat[y] = mat[pre[y]];
}
ll sum;
void KM() {
    for (int i = 1; i <= n; i++)
        bfs(i);
    for (int i = 1; i <= n; i++)
        sum += a[mat[i]][i];
    printf("%lld\n", sum);
    for (int i = 1; i <= n; ++i)
        printf("%d%c", mat[i], i == n ? '\n' : ' ');
}