零、基本思想
- 将输入数据转换为有向图，并使用tarjan算法求得图中的所有scc，再判断已知条件是否自相矛盾（即判断每一点是否与它的反点位于同一个scc中，如果是则问题无解）
一、转换方式
- 在一般的逻辑推理中，我们所能依靠的只有"必然"的联系。例如：A和B中有且仅有一个是杀手，则无论A和B哪个是杀手，在已知一人是杀手后，另一人都不可能是杀手。通过依赖这种"不可能"的关系，也就是给定条件间的自我矛盾，也就可以进行建图和问题求解了。
二、判断2-SAT问题中一组可行解的方法
- 对有向图进行Tarjan缩点后，再对于每一个可能性（每个可能性分为了两个点）判断两点属于的scc序号大小，取序号较大的作为可行解的一部分（由2-SAT问题的对称性和tarjan算法的递归加点过程即可证明算法的正确性）