算法流程
x0 ---> y1 表示x为false时y必须为true
最后输出的时候谁的bel小选谁
前后缀建图
例：要求n个变量满足至多有1个为true。
暴力：一个点的true向其它n-1个点的false连边，复杂度O(n^2)。
正解：prei表示前i个点是否有真。
prei的true向prei+1的true连边，prei+1的false向prei的false连边。
prei向i+1的false连边，i+1的true向prei的false连边。
i的true向prei的true连边，prei的false向i的false连边。
然后2-sat即可。
解决多元限制的方法通常是找性质+暴力枚举
例：
sol：手玩一下每个点的方程可以发现一些性质。
即每个点都可以用A(1,1)和第一行，第一列的各一个变量以及B矩阵来表示。
枚举A(1,1)后就可以2-sat了。