到今天总算是刷完了poj的6道2-sat，在这里做个纪念。
2-sat的本质就是给你n个布尔变量和m个限制，限制一共有四种格式：
一般要求求出是否可同时满足这m个限制，或是求出一组同时满足这些限制的解。
一般的解法是，对于每个布尔变量ai，我们把它拆成两个点ai和ai’，分别代表为真和为假的状态。于是原题就变成了在2n个点中选取n个点。
然后对于上述4种限制，我们可以转换并连边为
同时需要注意到，由于每个变量只可能同时有一个状态（即2-sat的对称性），当我们连了一条A到B’的边时，我们还必须连一条B到A’的边。因为选A就必须选B，若选了B’再选A的话我们还要选B，而B和B’是无法同时选的。其他的连边类似。
特殊的，在某种情况下我们会遇到必须选A的情景。这时候我们可以连一条由A’到A的边，限制住必须选A。
将边都连完后，我们就得到了一张有向图，这张图中可能一些环，因此我们需要缩点。我们用tarjan求出所有的强连通分量，易得在同一个强连通分量中的点要么同时都选，要么同时都不选。因此我们只要看一下有没有对应点存在于同一个强连通分量中即可判断是否有解（因为每对对应点都必须选且只能选一个）。
对于要求输出一组解的情况，一般的方法是对已缩完点的图建立反图，对反图进行拓扑排序然后染色，将出度为0的点染成红色，并将它们的对应点以及其前驱都染成蓝色，当所有点都染色完毕后，所有红色的点就是一组解。
然而还有更简便的方法：当我们用tarjan进行缩点的时候，所有强连通分量求出的顺序就是原图的逆拓扑序，由此我们省略了建立反图和拓扑排序。再者，根据2-sat的对称性，对于每一对对应点我们都选所在联通块时间戳更小的，这样对于大的那个点，其前驱必定是所在点对中时间戳大的。这样，我们只需一遍tarjan即可求出一组解。
对于一些题目，要求求出字典序最小的点。对于这样的题目，我们无法缩点解决，似乎唯一可行的方案就是爆搜。。。不过poj的六道题中是没有这样的题的。
PS:对于2-sat的一些更专业的介绍和对称性的证明可以参考《由对称性解2-SAT问 题》（伍昱）和《2-SAT解法浅析》（赵爽）
反正我是看不懂就是了
附上poj上的6到题以及我的渣题解