每个变量x拆成x0、x1,分别代表true/flase
若由x=0可以推导出y=0,则由x0向y0连边
分犯人
为每个犯人xi建一个虚拟节点Yi
从大到小处理犯人之间的关系
若使xi与xj分到不同监狱：合并xi与yj
使用2-sat建立约束： x xor y =0
因此所有的连边都是双向边
所以维护强连通分量转化为连通分量
tarjan可优化为并查集
多元多会最短路问题：建超级起点和超级终点（各起点到超级起点边权为零），转化成单元单会
二进制分组：枚举二进制位，将s个数按枚举的位是0和1分为两组，这样可以不重不漏
P2296
从终点反跑dfs标记所有跑到的点
删去无标记的点
删去所有指向无标记点的点
正向跑dij
优化建图