题解
Let’s build for both 2-SAT formulas implication graph and let’s find strong connected components in this graph. If both of the formulas are not satisfiable then the answer is SIMILAR. If only one formula is not satisfiable then we can find an answer for the second one and output it. Now, let’s assume both formulas are satisfiable. Let’s have a transitive closure for both of the graphs. Let’s call the variable X fixed in the formula F if there is a path -> x or (x -> ). If there is a fixed variable in one formula, but not fixed in the other (or fixed but has other value) we can find the solution for that second formula with opposite value of that fixed variable — that will be an answer. If we could not find these variables, we can remove all of them. There is no fixed variables in the rest of them. Let’s find an edge u->v, presented in one graph, but not presented in the other. Let’s find the solution for formula without the edge with u = 1 and v = 0 (we always can find it). That is the answer.
大概意思就是说 我们先看 f 和 g 是不是都有解 不是的话就输出 然后再考虑 f 和 g 确定值的变量的集合 S 是不是相同的 不是的话也有解 然后删去 S 的所有变量 再看 f 是不是有路径 u−v 而 g 没有 那么也能构造出 u 和 反 v <script type="math/tex" id="MathJax-Element-305">v</script> 的解 否则就输出SIMILAR
#include<cstdio> #include<cstdlib> #include<algorithm> #include<bitset> using namespace std; const int N=2005; struct SAT{ int n,m,sol; int c[N]; bitset<N> g[N]; void read(int _n,int _m){ int iu,iv; n=_n; m=_m; for (int i=1;i<=m;i++){ scanf("%d%d",&iu,&iv); if (iu>0) iu=(iu-1)<<1|1; else iu=(-iu-1)<<1; if (iv>0) iv=(iv-1)<<1|1; else iv=(-iv-1)<<1; g[iu^1][iv]=g[iv^1][iu]=1; } for (int i=0;i<(n<<1);i++) g[i][i]=1; for (int k=0;k<(n<<1);k++) for (int i=0;i<(n<<1);i++) if (g[i][k]) g[i]|=g[k]; sol=1; for (int i=0;i<(n<<1);i++) if (g[i][i^1] && g[i^1][i]) sol=0; if (sol){ for (int i=0;i<(n<<1);i++) c[i]=-1; for (int i=0;i<(n<<1);i++) if (g[i][i^1]) color(i^1); } } void color(int u){ if (~c[u]) return; c[u]=1; c[u^1]=0; for (int v=0;v<(n<<1);v++) if (g[u][v]) color(v); } void solve(int c1=-1,int c2=-1){ if (~c1) color(c1); if (~c2) color(c2); for (int i=0;i<(n<<1);i++) if (c[i]==-1) color(i); for (int i=0;i<n;i++) c[i<<1]?printf("0 "):printf("1 "); } }f,g; int n,m1,m2; inline bool Solve(SAT &f,SAT &g){ if (!f.sol) return 0; if (!g.sol) return f.solve(),1; for (int i=0;i<(n<<1);i++) if (f.c[i]!=0 && g.c[i]==0) return f.solve(i),1; for (int i=0;i<(n<<1);i++) if (f.c[i]==-1) for (int j=0;j<(n<<1);j++) if (f.c[j]==-1) if (!f.g[i][j] && g.g[i][j]) return f.solve(i,j^1),1; return 0; } int main(){ freopen("t.in","r",stdin); freopen("t.out","w",stdout); scanf("%d%d%d",&n,&m1,&m2); f.read(n,m1); g.read(n,m2); if (!Solve(f,g) && !Solve(g,f)) printf("SIMILAR\n"); return 0; }