证明正确性时发现有解情况下 x 和 -x 在缩完点的 DAG 上不存在 x -> -x 或 -x -> x 的路径，请问这是对的吗？
理由大概就是 2-sat 的图是对称的，如果 x -> -x 则必然可以通过对称得到 -x -> x，与有解矛盾。
