转载：http://blog.csdn.net/luyuncheng/article/details/15172827
此题好纠结啊。。。其实2-sat关键是建边
此题网上好多题解都是直接说了建边而且建边完全没有解释清楚，说了的也都是模模糊糊完全不能让人信服啊啊啊啊
反正我是没有找到一个能让我完全理解的
索性自己想了下，我的建边以及证明如下:
因为公式不好贴，我有些是发的图有些是自己打的符号，复制粘贴的时候难免有问题，还有就是貌似网页字符有时候会和我自己手打的符号产生矛盾，会显示不出来，如有问题请指出。
说先说下2-sat
对于布尔方程的合取范式:(a∨b∨。。。)∧(c∨d。。。)
中a，b，。。。称为文字，他是一个布尔变量或其否定，像(a∨b∨。。。)这样用∨析取连接的部分称为子句。如果合取范式的每个子句中的文字个数都不超过两个，那么对应的sat问题称为2-sat问题
建边问题，首先利用=>蕴涵表达式将每个子句(a∨b)改写成等价形式
。这样原布尔公式就变成了把(a=>b)形式的布尔公式用∧连接起来的形式。对每个布尔变量x，构造两个顶点分别代表x和~x，以=>关系为边建立有向图。此时，如果图上的a点能够达到b点的话，就表示当a为真时b也一定为真。因此，该图中同一个强连通分量中所含的所有文字的布尔值均相同。
如果存在某个布尔变量x，x和~x均在同一个强连通分量中，则显然无法令整个布尔公式的值为真，反正，如果不存在这样的布尔变量，那么对于每个布尔变量x，让
X所在的强连通分量的拓扑序在~x所在的强连通分量之后 < =>x为真
以上摘自《挑战程序设计竞赛》
好，现在我们还要将逻辑语句化成范式
AND语句就是自己本身的范式A∧B
a AND b==1:(a∨a)∧(b∨b)
a AND b==0:(~a∨~b)∧(~b∨a)
OR语句可以看成a∨b
a OR b==1:就是上面的(a∨b)等价形式
a OR b==0:换成合取范式为1的可以全部取非 化成~a∧~b
然后可以看成 (~a∨~a)∧(~b∨~b)
异或语句也是最难的:
首先异或操作可以看成:a XOR b == ~(a <–> b)
== ~ [ (a->b)∧(b->a) ]
== ~ [ (~ a ∨ b)∧(~ b ∨ a) ]
== [~(~a∨b)] ∨ [~(~b∨a)]
== (a∧~b) ∨ (b ∧ ~a)
得到析取范式：(a∧~b) ∨ (b ∧ ~a)
然后转换成合取范式（这里我不知道公式，望大神指教公式。我是用分配率一个个换进去的）
(a∧~b) ∨ (b ∧ ~a) ==[ (a∧~b)∨b ] ∧ [ (a∧~b)∨~a ]
==(b∨a)∧(b∨~b)∧(~a∨a)∧(~a∨~b)
好了如果a XOR b ==1 有(b∨a)∧(b∨~b)∧(~a∨a)∧(~a∨~b)
a XOR b ==0 由于前面那个退单范式中有个是因为前面加了~的
所以取~就是: (~a∨b)∧(~b∨a)
好了现在开始建边了
建边就根据前面说的对于每个(a∨b),~a连边到b.~b连边到a.
这也就是
a and b ==1 : ~a->a , ~b -> b
a and b ==0 : a->~b , b->~a
a or b ==1 : ~a->b , ~b->a
a or b ==0 : a->~a , b->~b
a xor b ==1 : a->~b,~b->a,~a->b,b->~a
a xor b ==0 : a->b,b->a,~a->~b,~b->~a
那么hdu4421就是将每一个int32的整数每一位拿出来做同样的操作就好了