前后缀建图

例：要求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了。