众所周知，2—SAT是一个很冷门的模型（冷门到连百度百科好像都没有收录），但又是一种很有用的思想，比如[NOI2017]游戏,原题是NPC问题，属于3—SAT的范畴，但是如果用一些骚操作（用DFS先确定一种车车和道路）。
话不多说，回正题（不知道什么是2-SAT模型的童鞋们建议先百度一下，学会TARJAN求2-SAT的一组解吧）。
2-SAT模型可以求出一组合法的解，而所谓最小答案序列是指选取的元素的字典序最小的答案序列。
下面我们来谈一谈染色法（这里必须要先学会TARJAN算法）。
所谓染色法分为两个部分：
1.主体（废话）
2.DFS判定函数
先放一下代码吧：
bool DFS(int x) { if(vis[x^1]) return false; if(vis[x]) { return true; } vis[x]=true; stack[++cnt]=x; for(int i=0;i<b[x].size();i++) { int to=b[x][i]; if(!DFS(to)) return false; } return true; } bool SAT2(int n) { for(int i=2;i<n;i+=2) { if(vis[i]||vis[i^1]) continue; cnt=0; if(!DFS(i)) { while(cnt) { vis[stack[cnt--]]=0; } if(!DFS(i^1)) return false; } } return true; }
代码中两个关联点的关系是靠异或连接，因此2，3代表第1个元素的两个选择，4，5代表第二个元素的两个选择
众所周知，2—SAT互相限制的实现方法是建图，如果选A必须选B，那么就从A向B拉一条有向边。
因为我们要求答案的字典序最小，所以我们对于每一个元素优先考虑第一个选择。
看代码：
1.枚举每一个元素，记该元素的两个选择为I和I^1
2.先检查I或者I^1是否因为之前的元素导致必须要选，如果是，就不用找了。
3.对I进行DFS判断，如果不能满足，消除判断过程的影响（具体影响是什么下面在DFS中解释），如果满足，直接返回1（因为I一定要小于I^1,满足字典序最小）。
4.对I^1进行DFS判断，如果仍然不合法，直接返回0（I和I^1都无法满足之前的限制条件）。
下面我们来看DFS函数是如何判断元素X是否可以满足当前2—SAT的限定条件的。
1.先看X和X^1是否已经被之前的条件强制要求
2.若两者均不，将X打上标记，塞入栈中，并且对X所要求的条件进行DFS判定，如果X所要求的条件均合法，那么X就是合法的返回1否则返回0。
至于中间的栈存的是什么：因为如果在对X所要求的条件进行判定的过程中，如果有一些条件是因为X才受到限制的（也就是说原来的这个状态单独拿出来是两个选择均可的），那么，在对X进行判定的过程中，这些点的状态均会被锁定，如果最后X没能成功满足2—SAT，选不得，那么我们需要对上述特殊点的状态进行复原（由锁定某一状态变成任意状态均可）。至于为啥不需要对DFS(X^1)同样进行复原，你怕不是傻！！！（如果X^1判定成功了就不需要复原，如果同样失败了，那整个2-SAT就说明不可能满足要求）。
重点：
这里实际上是林荫在思考中产生的一个问题，按照这个算法的思路，假设两元组(A1,A2)是一个元素的两种选择，那么按照贪心的思想，在当前能选A1的情况下一定选A1，但是如果出现了下面的情况？有形同上的二元组A,B,且A1不得与B1,B2同时出现。按照算法的思想，优先选择A1，那么会不会导致这组数据被判定无解呢？
NO！！！
因为我们首先对加边过程进行考虑，A1有向B2,B1连的边（因为A1不与B1同时出现，A1连B2，因为A1不用B2同时出现，A1连B1）。这样，在对于A1的判定中，先进入B2，给vis[B2]打上标记，然后进入B1，因为vis[B1^1]==vis[B2]==1,这样对于B1的判定会返回0，然后对于A1的判定会返回0，只能开始对A2的判定。
这样的话，基本就解决了，给个例题吧：
代码我直接贴了：
#include<iostream> #include<cstdio> #include<algorithm> #include<vector> #include<cstring> using namespace std; int n,m; vector<int> b[16101]; int a1,a2; int vis[16101],stack[16101]; int num,cnt,qlt; bool DFS(int x) { if(vis[x^1]) return false; if(vis[x]) { return true; } vis[x]=true; stack[++cnt]=x; for(int i=0;i<b[x].size();i++) { int to=b[x][i]; if(!DFS(to)) return false; } return true; } bool SAT2(int n) { for(int i=2;i<n;i+=2) { if(vis[i]||vis[i^1]) continue; cnt=0; if(!DFS(i)) { while(cnt) { vis[stack[cnt--]]=0; } if(!DFS(i^1)) return false; } } return true; } void LINYIN() { for(int i=1;i<=n*2+2;i++) { b[i].clear(); } memset(stack,0,sizeof(stack)); memset(vis,0,sizeof(vis)); cnt=0; for(int i=1;i<=m;i++) { scanf("%d%d",&a1,&a2); a1++; a2++; b[a1].push_back(a2^1); b[a2].push_back(a1^1); } if(SAT2(n*2+2)) { for(int i=2;i<n*2+2;i++) { if(vis[i]) printf("%d ",i-1); } } else printf("NIE "); return ; } int main() { while(~scanf("%d%d",&n,&m)) { LINYIN(); } return 0; }
完结撒花！！！