2-SAT

FJ_00460 · 2025-05-04 19:18:05 · 算法·理论

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'同时被选取，如果不存在矛盾，那么当前问题就是有解的。