2-SAT

定义

• 搞出 $N$个集合，每个集合2个元素
• 若干个$<a, b>$表示$a, b$矛盾（$a, b$属于不同集合）
• 然后从每个集合选择一个元素，一共选$n$个两两不矛盾的元素
• 有多钟方案

布尔可满足性

• 给定一条真值表达式，包括逻辑变量，逻辑与，或，非
• 是否存在一组对这些变量的赋值，使整条式子结果为 $true$?
• 如果可以，就是这条公式的布尔可满足性。

流程

• 通过连边建图（理解上的难点）
• 求图的极大强联通子图($tarjan$)
• 把每个子图收缩成单个节点，根据原图关系构造一个有向无环图
• 判断是否有解，无解就输出（二分）
• 对新图拓补排序
• 自低向上选择，删除
• 输出

建图

• 利用有向边$<i, j>$ 表示选了$i$，必须选$j$
• $i$ 表示某个点是$true$，那么$i'$表示某个点是$false$
• 因为限制了关系，所以可以逻辑建边
  • 如果给出$a, b$限制关系，$a, b$必须一起选，$(a \lor b) || (!a \lor !b) == true$那么选a必选b，建边$<i, j>, <j, i>$ 还有 $<i', j'>, <j', i'>$
  • 如果给出$a, b$限制关系，$a, b$不能一起选，那么$(a \lor !b) || (!a \lor b) == true$，建边$<i, j'>, <j, i'>$
  • 如果必须选a，那么$a == true$，建边$<i', i>$
  • 如果a一定不选，那么 $!a == true$，建边$<i, i'>$
• 这样，出现有向图
• 如果能找到一个强联通分量，那么这个强联通分量中的点，若选取必须全部选取，不选取一定全不选取。
• 只要满足这个有向图中联通的点不会导致$i, i'$同时被选取，如果不存在矛盾，那么当前问题就是有解的。