{TwoSAT}

Posted 2020-09-29 yijiull

今天学习图论的时候，碰到了2sat问题

虽然不是很难理解，感觉很精妙 ▄█?█●

用的LRJ白书上的模板。

套路如下：

　　 2 - SAT就是2判定性问题，是一种特殊的逻辑判定问题。

　　选择的置为1，未选的置为0

　　对于2SAT，每组矛盾都会有四种情况（2*2），题目会限制一种不成立，我们要做的就是找出这一种，用逻辑连接词表示出来，然后取反，加边即可。

　　具体过程白书上p324有讲，这里就不说了。

　　下面附三道题，做做就知道套路了

Party

 HDU - 3062 

 1 #include <bits/stdc++.h>
 2 using namespace std;
 3 const int maxn=1010;
 4 struct TwoSAT
 5 {
 6     int n;
 7     vector<int> G[maxn<<1];
 8     bool mark[maxn<<1];
 9     int s[maxn<<1],c;
10 
11     bool dfs(int x)
12     {
13         if(mark[x^1]) return false;
14         if(mark[x]) return true;
15         mark[x]=true;
16         s[c++]=x;
17         for(int i=0;i<G[x].size();i++)
18             if(!dfs(G[x][i])) return false;
19         return true;
20     }
21 
22     void init(int n)
23     {
24         this->n=n;
25         for(int i=0;i<n*2;i++) G[i].clear();
26         memset(mark,0,sizeof(mark));
27     }
28 
29     void add_clause(int x,int xv,int y,int yv)
30     {
31         x=x*2+xv;
32         y=y*2+yv;
33         G[x^1].push_back(y);
34         G[y^1].push_back(x);
35     }
36 
37     bool solve()
38     {
39         for(int i=0;i<n*2;i+=2)
40             if(!mark[i]&&!mark[i^1])
41             {
42                 c=0;
43                 if(!dfs(i))
44                 {
45                     while(c>0) mark[s[--c]]=false;
46                     if(!dfs(i+1)) return false;
47                 }
48             }
49         return true;
50     }
51 }solver;
52 int n,m;
53 int age[maxn],sum;
54 
55 
56 int main()
57 {
58     while(scanf("%d%d",&n,&m)!=EOF)
59     {
60         int x,y,a,b;
61         solver.init(n);
62         for(int i=0;i<m;i++)
63         {
64            scanf("%d%d%d%d",&a,&b,&x,&y);
65            solver.add_clause(a,x^1,b,y^1);
66         }
67         if(solver.solve()) puts("YES");
68         else puts("NO");
69     }
70     return 0;
71 
72 
73 }

View Code

 

Now or later

 UVALive - 3211

 1 #include <bits/stdc++.h>
 2 using namespace std;
 3 const int maxn=2010;
 4 struct TwoSAT
 5 {
 6     int n;
 7     vector<int> G[maxn<<1];
 8     bool mark[maxn<<1];
 9     int s[maxn<<1],c;
10 
11     bool dfs(int x)
12     {
13         if(mark[x^1]) return false;
14         if(mark[x]) return true;
15         mark[x]=true;
16         s[c++]=x;
17         for(int i=0;i<G[x].size();i++)
18             if(!dfs(G[x][i])) return false;
19         return true;
20     }
21 
22     void init(int n)
23     {
24         this->n=n;
25         for(int i=0;i<n*2;i++) G[i].clear();
26         memset(mark,0,sizeof(mark));
27     }
28 
29     void add_clause(int x,int xv,int y,int yv)
30     {
31         x=x*2+xv;
32         y=y*2+yv;
33         G[x^1].push_back(y);
34         G[y^1].push_back(x);
35     }
36 
37     bool solve()
38     {
39         for(int i=0;i<n*2;i+=2)
40             if(!mark[i]&&!mark[i^1])
41             {
42                 c=0;
43                 if(!dfs(i))
44                 {
45                     while(c>0) mark[s[--c]]=false;
46                     if(!dfs(i+1)) return false;
47                 }
48             }
49         return true;
50     }
51 }solver;
52 int n;
53 int T[maxn][2];
54 
55 bool test(int diff)
56 {
57     solver.init(n);
58     for(int i=0;i<n;i++) for(int a=0;a<2;a++)
59         for(int j=i+1;j<n;j++) for(int b=0;b<2;b++)
60         if(abs(T[i][a]-T[j][b])<diff) solver.add_clause(i,a^1,j,b^1);
61     return solver.solve();
62 }
63 
64 int main()
65 {
66     while(scanf("%d",&n)==1&&n)
67     {
68         int L=0,R=0;
69         for(int i=0;i<n;i++) for(int a=0;a<2;a++)
70         {
71             scanf("%d",&T[i][a]);
72             R=max(R,T[i][a]);
73         }
74         while(L<R)
75         {
76             int M=(R-L+1)/2+L;
77             if(test(M)) L=M;
78             else R=M-1;
79         }
80         printf("%d\n",L);
81     }
82     return 0;
83 
84 }

View Code

 

Astronauts

 UVALive - 3713

 1 #include <bits/stdc++.h>
 2 using namespace std;
 3 const int maxn=100010;
 4 struct TwoSAT
 5 {
 6     int n;
 7     vector<int> G[maxn<<1];
 8     bool mark[maxn<<1];
 9     int s[maxn<<1],c;
10 
11     bool dfs(int x)
12     {
13         if(mark[x^1]) return false;
14         if(mark[x]) return true;
15         mark[x]=true;
16         s[c++]=x;
17         for(int i=0;i<G[x].size();i++)
18             if(!dfs(G[x][i])) return false;
19         return true;
20     }
21 
22     void init(int n)
23     {
24         this->n=n;
25         for(int i=0;i<n*2;i++) G[i].clear();
26         memset(mark,0,sizeof(mark));
27     }
28 
29     void add_clause(int x,int xv,int y,int yv)
30     {
31         x=x*2+xv;
32         y=y*2+yv;
33         G[x^1].push_back(y);
34         G[y^1].push_back(x);
35     }
36 
37     bool solve()
38     {
39         for(int i=0;i<n*2;i+=2)
40             if(!mark[i]&&!mark[i^1])
41             {
42                 c=0;
43                 if(!dfs(i))
44                 {
45                     while(c>0) mark[s[--c]]=false;
46                     if(!dfs(i+1)) return false;
47                 }
48             }
49         return true;
50     }
51 }solver;
52 int n,m;
53 int age[maxn],sum;
54 
55 bool check(int x)
56 {
57     return age[x]*n<sum;
58 }
59 
60 int main()
61 {
62     while(scanf("%d%d",&n,&m)!=EOF&&(n||m))
63     {
64         sum=0;
65         for(int i=0;i<n;i++) {
66             scanf("%d",&age[i]);
67             sum+=age[i];
68         }
69         solver.init(n);
70         for(int i=0;i<m;i++)
71         {
72             int a,b;
73             scanf("%d%d",&a,&b);
74             a--;b--;
75             solver.add_clause(a,1,b,1);
76             if(check(a)==check(b)) solver.add_clause(a,0,b,0);
77         }
78         if(!solver.solve()) printf("No solution\n");
79         else {
80             for(int i=0;i<n;i++)
81             if(solver.mark[i*2]) printf("C\n");
82             else if(check(i)) puts("B");
83             else puts("A");
84         }
85     }
86     return 0;
87 }

View Code

 

基本都一样的套路。。。