部分参照：From:http://blog.csdn.net/jarjingx/article/details/8521690
综述：每个条件的形式都是x[i]为真/假或者x[j]为真/假，
每个x[i]拆成2*i和2*i+1两个点，分别表示x[i]为真，x[i]
为假；加的每一条边之间的关系是and
模型一：两者（A，B）不能同时取（但可以两个都不选）
说明：A 为假或 B 为假
那么选择了 A 就只能选择 B’，选择了 B 就只能选择 A’
连边 A→B’，B→A’
模型二：两者（A，B）不能同时不取（但可以两个都选）
说明：A 为真或 B 为真
那么选择了 A’就只能选择 B，选择了 B’就只能选择 A
连边 A’→B，B’→A
模型三：两者（A，B）要么都取，要么都不取
说明：......
那么选择了 A，就只能选择 B，选择了 B 就只能选择 A，选择了 A’就只能选择 B’，
选择了 B’就只能选择 A’
连边 A→B，B→A，A’→B’，B’→A’
模型四：两者（A，A’）必取A
那么，那么，该怎么说呢？先说连边吧。
连边 A’→A
模型五（补充） ：两者（A，B）两个必须不相同，即要么选A，要么选B
逻辑表达：A||B 非 A||非 B
连边：A 为真或 B 为真： A’--->B B’--->A;
A 为假或 B 为假: A-->B’ B-->A
说明：A 或 B，非 A 或非 B，前者表示两者至少有一个 true，后者表示至少有一个 false
这5种矛盾关系基本全面了，在逻辑混乱的时候可以作为一个傻瓜式的参考！！！
附：2-sat+二分答案体型的统一建模方式（编码简短、正确率略高）
2-sat+二分答案
现在统一建模的方式：
1、同一组的两个状态分别存储在2*i和2*i+1两个节点，产生2*n个节点
2、for(int i=1;i<2*n;i++)
for(int j=0;j<i;j++)
{
if (i==(j^1)) continue;//记得j^1加上小括号
sat.add_clause(i,j);//枚举出的不属于同一组的不相容的两点
}