2-Sat+输出可行解(个人模版)

时间:2022-05-07
本文章向大家介绍2-Sat+输出可行解(个人模版),主要内容包括其使用实例、应用技巧、基本知识点总结和需要注意事项,具有一定的参考价值,需要的朋友可以参考一下。

2-Sat+输出可行解:

  1 //LightOJ 1251
  2 #include<stdio.h>
  3 #include<string.h>
  4 #include<vector>
  5 #include<queue>
  6 using namespace std;
  7 int output[40005];
  8 int vis[70005];
  9 int low[70005];
 10 int dfn[70005];
 11 int print[70005];
 12 int stack[70005];
 13 int color[70005];
 14 int pos[70005];
 15 int degree[70005];
 16 vector<int >mp[70005];
 17 vector<int >mp2[70005];
 18 int n,m,sig,cnt,tot,cont;
 19 void add(int x,int y)
 20 {
 21     mp[x].push_back(y);
 22 }
 23 void top()
 24 {
 25     memset(print,0,sizeof(print));
 26     queue<int >s;
 27     for(int i=1;i<=sig;i++)
 28     {
 29         if(degree[i]==0)
 30         {
 31             s.push(i);
 32         }
 33     }
 34     while(!s.empty())
 35     {
 36         int u=s.front();
 37         if(print[u]==0)
 38         {
 39             print[u]=1;print[pos[u]]=2;
 40         }
 41         s.pop();
 42         for(int i=0;i<mp2[u].size();i++)
 43         {
 44             int v=mp2[u][i];
 45             degree[v]--;
 46             if(degree[v]==0)s.push(v);
 47         }
 48     }
 49     cont=0;
 50     for(int i=1;i<=n;i++)if(print[color[i]]==1)output[cont++]=i;
 51 }
 52 void Tarjan(int u)
 53 {
 54     vis[u]=1;
 55     dfn[u]=low[u]=cnt++;
 56     stack[++tot]=u;
 57     for(int i=0;i<mp[u].size();i++)
 58     {
 59         int v=mp[u][i];
 60         if(vis[v]==0)Tarjan(v);
 61         if(vis[v]==1)low[u]=min(low[u],low[v]);
 62     }
 63     if(low[u]==dfn[u])
 64     {
 65         sig++;
 66         do
 67         {
 68             vis[stack[tot]]=-1;
 69             color[stack[tot]]=sig;
 70         }
 71         while(stack[tot--]!=u);
 72     }
 73 }
 74 int Slove()
 75 {
 76     sig=0;
 77     cnt=1;
 78     tot=-1;
 79     memset(degree,0,sizeof(degree));
 80     memset(stack,0,sizeof(stack));
 81     memset(dfn,0,sizeof(dfn));
 82     memset(low,0,sizeof(low));
 83     memset(vis,0,sizeof(vis));
 84     memset(color,0,sizeof(color));
 85     for(int i=1;i<=n*2;i++)
 86     {
 87         if(vis[i]==0)
 88         {
 89             Tarjan(i);
 90         }
 91     }
 92     for(int i=1;i<=n;i++)
 93     {
 94         if(color[i]==color[i+n])return 0;
 95         pos[color[i]]=color[i+n];
 96         pos[color[i+n]]=color[i];
 97     }
 98     for(int i=1;i<=n*2;i++)
 99     {
100         for(int j=0;j<mp[i].size();j++)
101         {
102             int v=mp[i][j];
103             if(color[i]!=color[v])
104             {
105                 degree[color[i]]++;
106                 mp2[color[v]].push_back(color[i]);
107             }
108         }
109     }
110     top();
111     return 1;
112 }
113 int main()
114 {
115     int t;
116     int kase=0;
117     scanf("%d",&t);
118     while(t--)
119     {
120         scanf("%d%d",&m,&n);
121         for(int i=1;i<=60000;i++)mp[i].clear(),mp2[i].clear();
122         for(int i=0;i<m;i++)
123         {
124             int x,y;
125             scanf("%d%d",&x,&y);
126             int xx=x;int yy=y;
127             if(x<0)x=-x;
128             if(y<0)y=-y;
129             if(xx>0&&yy>0)add(x+n,y),add(y+n,x);
130             if(xx>0&&yy<0)add(x+n,y+n),add(y,x);
131             if(xx<0&&yy>0)add(x,y),add(y+n,x+n);
132             if(xx<0&&yy<0)add(x,y+n),add(y,x+n);
133         }
134         int ans=Slove();
135         printf("Case %d: ",++kase);
136         if(ans==1)
137         {
138             printf("Yesn");
139             printf("%d",cont);
140             for(int i=0;i<cont;i++)
141             {
142                 printf(" %d",output[i]);
143             }
144             printf("n");
145         }
146         else printf("Non");
147     }
148 }