2-SAT问题

大家好，欢迎来到IT知识分享网。

2-SAT问题

SAT问题即适定性问题：是否可以确定一个满足所有条件的方案。

SAT问题的表述：有若干个集合，每个集合里有若干个元素，每个集合只能选择一个，然后再给出一些取元素的规则，问能否可行，能则给出一个可行方案。在所有集合中，元素个数最多的集合的元素个数为k个，则就称为K-SAT问题。所以2-SAT问题就是k=2时的情况，而当k>2时的情况已经被证明为NP完全问题。

学习资料：由对称性解2-SAT问题, 2-SAT解法浅析。

解决2-SAT问题的首要任务是构图，而构图的关键是找到冲突，而在构图中的边u->v表示选择u元素必须选择v元素，只要将题目中所述的关系都抽象出来建图就能够进行解决了。

构图之后则需要求强连通分量，一个强连通分量表示里面的所有点都相互可达，则表明选择其中一个点就必须选择其中的所有点，则此时就可以判断此2-SAT问题有没有解了：假如有两个矛盾点(属于同一个集合的两个元素而非题目给出的冲突)在同一个强连通分量则无解，否则就记录强连通块之间的矛盾(两个矛盾的元素属于两个不同的强连通块，则这两个块就是矛盾的)，方便缩点之后的求解。

所以之后再根据强连通分量进行缩点，然后将新图的边反向再建图。

为什么反向？

因为此时缩点后的新图仍然是传递选择标记的即选择当前节点之后其后代节点也都要被连带选择。如果此时进行拓扑排序的话那么最前面的祖先(在缩点后的新图入度为0)就会排在拓扑序列前面，而我们需要的是最后面的子孙(在缩点后的新图出度为0)应该排在前面，因为先对祖先染色的话，由于其后代都未被染色，所以要对其所有后代进行连带染色。而先对子孙染色的话就不会有连带效应，因为此时已经没有它能到达的后代节点存在所以不需要对后代进行连带染色。
而且如果不反向会导致无解。即对祖先先染色的话，对它直接确定的话对整个的后续选择影响太大，它会导致后续点的矛盾(即选择标记和不选择标记会传到相同的点)，详细解释看这位神犇。

反向建图之后再进行一次拓扑排序，然后根据拓扑序列对未染色的点进行染色(选择标记)，每次染色都要对与其矛盾的点进行染另一种颜色(不选择标记)，并对其所有的后代进行传递不选择标记。还可以在拓扑排序的过程中进行染色，这样效率比上述方法高，具体操作见代码。

进行完上述操作之后，被染为选择标记的强连通块所包含的所有点就是一个2-SAT解决方案。

在2-SAT问题中，关键部分在于对限制关系的抽象，其实主要就那么几种，根据现实语义去抽象即可。

①a, b不能同时选: 选a只能选b’，选b只能选a’。
②a, b必须同时选: 选a只能选b，选b只能选a，选a’只能选b’，选b’只能选a’。
③a, b至少选一个(不能同时不选): 选a’只能选b，选b’只能选a。
④a, b必须选且只能选一个: 选a只能选b’，选b只能选a’，选a’只能选b，选b’只能选a。
⑤a必须选: 加边a’->a，加这条边起到两个作用：一个是判断有无解，即若有条件a’也必须选，就会存在a->a’这条边，则它俩会属于同一个强连通分量，被判无解。另一个作用则是如果有解，则保证了在反图中进行拓扑排序后的拓扑序列中a是在a’的前面的，则实现了必选a的目的。(解释还是这位神犇)
限制关系还可以看看kuangbin。

下面两个模板以POJ-3683为例, 除了mapping部分构图, 其它算作模板直接使用。

输出任意一组可行解(O(M))：

#include <algorithm> #include <string.h> #include <cstdio> #include <queue> using namespace std; const int maxn = 1005*2; const int maxm = maxn*maxn; struct node { int u, v, next; } edge[maxm], new_edge[maxm]; int no, new_no, head[maxn]; int n; char s[maxn][2][10]; int tim[maxn][2], limit[maxn]; int index, top; int dfn[maxn], low[maxn], stack[maxn], vis[maxn]; int cnt; int belong[maxn]; queue<int> q; int opp[maxn], deg[maxn], color[maxn]; inline void init() { no = 0; memset(head, -1, sizeof head); index = top = 0; memset(dfn, 0, sizeof dfn); memset(vis, 0, sizeof vis); new_no = 0; memset(deg, 0, sizeof deg); memset(color, 0, sizeof color); } inline void add(int u, int v) { edge[no].u = u, edge[no].v = v; edge[no].next = head[u]; head[u] = no++; } inline void new_add(int u, int v) { new_edge[new_no].u = u, new_edge[new_no].v = v; new_edge[new_no].next = head[u]; head[u] = new_no++; } void mapping() { int hh, mm, minn, maxx; scanf("%d", &n); init(); for(int i = 0; i < n; ++i) { scanf("%s %s %d", s[i][0], s[i][1], &limit[i]); hh = (s[i][0][0]-'0')*10+(s[i][0][1]-'0'); mm = (s[i][0][3]-'0')*10+(s[i][0][4]-'0'); tim[i][0] = hh*60+mm; hh = (s[i][1][0]-'0')*10+(s[i][1][1]-'0'); mm = (s[i][1][3]-'0')*10+(s[i][1][4]-'0'); tim[i][1] = hh*60+mm; } for(int i = 0; i < n; ++i) for(int j = i+1; j < n; ++j) //根据题目把冲突抽象出来,然后建边 { minn = min(tim[i][0], tim[j][0]); maxx = max(tim[i][0]+limit[i], tim[j][0]+limit[j]); if(maxx-minn < limit[i]+limit[j]) { add(i*2, j*2+1); add(j*2, i*2+1); } minn = min(tim[i][0], tim[j][1]-limit[j]); maxx = max(tim[i][0]+limit[i], tim[j][1]); if(maxx-minn < limit[i]+limit[j]) { add(i*2, j*2); add(j*2+1, i*2+1); } minn = min(tim[i][1]-limit[i], tim[j][1]-limit[j]); maxx = max(tim[i][1], tim[j][1]); if(maxx-minn < limit[i]+limit[j]) { add(i*2+1, j*2); add(j*2+1, i*2); } minn = min(tim[i][1]-limit[i], tim[j][0]); maxx = max(tim[i][1], tim[j][0]+limit[j]); if(maxx-minn < limit[i]+limit[j]) { add(i*2+1, j*2+1); add(j*2, i*2); } } } void tarjan(int cur) //求强联通分量 { dfn[cur] = low[cur] = ++index; stack[++top] = cur; vis[cur] = 1; for(int k = head[cur]; k != -1; k = edge[k].next) { if(!dfn[edge[k].v]) { tarjan(edge[k].v); low[cur] = min(low[cur], low[edge[k].v]); } else if(vis[edge[k].v]) { low[cur] = min(low[cur], dfn[edge[k].v]); } } if(dfn[cur] == low[cur]) { ++cnt; do { vis[stack[top]] = 0; belong[stack[top]] = cnt; --top; } while(stack[top+1] != cur); } } void topsort() { memset(head, -1, sizeof head); for(int i = 0; i < no; ++i) //枚举所有边，进行缩点然后建立反向图 { int u = edge[i].u, v = edge[i].v; if(belong[u] == belong[v]) continue; new_add(belong[v], belong[u]); //建立反向边，其实可能会重复建边，但不会导致错误，如果检测重边的话则检测程序会比重边在使用过程中更加降低效率。 ++deg[belong[u]]; } while(!q.empty()) q.pop(); for(int i = 1; i <= cnt; ++i) if(!deg[i]) q.push(i); while(!q.empty()) { int u = q.front(); q.pop(); if(!color[u]) color[u] = 1, color[opp[u]] = -1; //这里不进行不选择标记的传递也可行，因为不必对不选择点进行相应的更改入度，所以其后代不选择点一定不影响 //选择点扩散，从而还形成了一个优化，即不必让所有点都进行入队。 int k = head[u]; while(k != -1) { if(--deg[new_edge[k].v] == 0) q.push(new_edge[k].v); k = new_edge[k].next; } } } void print() { for(int i = 0; i < n; ++i) { if(color[belong[i*2]] == 1) { int mm = tim[i][0]+limit[i]; printf("%s %02d:%02d\n", s[i][0], mm/60, mm%60); } if(color[belong[i*2+1]] == 1) { int mm = tim[i][1]-limit[i]; printf("%02d:%02d %s\n", mm/60, mm%60, s[i][1]); } } } void solve() { for(int i = 0; i < n*2; ++i) if(!dfn[i]) tarjan(i); for(int i = 0; i < n; ++i) { if(belong[i*2] == belong[i*2+1]) { puts("NO"); return ; //存在可行方案的充分条件：不存在同一个集合的两个元素属于同一个强连通分量 } else { opp[belong[i*2]] = belong[i*2+1]; opp[belong[i*2+1]] = belong[i*2]; //任意两组矛盾点，这两组中的各一个元素属于同一个强连通分量，则另外两个也必定属于同一个强连通分量(对称性)。 //所以每个强连通块的矛盾块有且只有一个，两个矛盾块存储的opp必定是对方 } } topsort(); puts("YES"); print(); } int main() { mapping(); //建边构图 solve(); return 0; }

输出字典序最小的一组解，时间复杂度不到O(NM)，但是不如上面的O(M)，但是题目要求输出字典序最小的一组解就只能选择这个了，以下操作能保证字典序最小。

如果原图中的同一对点编号都是连续的（01、23、45……）则可以依次尝试第0对、第1对……，每对点中先尝试编号小的，若失败再尝试编号大的。这样一定能求出字典序最小的解（如果有解的话）。

如果原图中的同一对点编号不连续（比如03、25、14……）则按照该对点中编号小的点的编号递增顺序将每对点排序，然后依次扫描排序后的每对点，先尝试其编号小的点，若成功则将这个点选上，否则尝试编号大的点，若成功则选上，否则（都失败）无解。

#include <algorithm> #include <string.h> #include <cstdio> using namespace std; const int maxn = 1005*2; const int maxm = maxn*maxn; struct node { int v, next; } edge[maxm]; int n; int no, head[maxn]; char s[maxn][2][10]; int tim[maxn][2], limit[maxn]; int top, S[maxn]; //用于标记的反悔的栈 int mark[maxn]; //2*n个点的标记 inline void init() { no = 0; memset(head, -1, sizeof head); top = 0; memset(mark, 0, sizeof mark); } inline void add(int u, int v) { edge[no].v = v; edge[no].next = head[u]; head[u] = no++; } void mapping() { int hh, mm, minn, maxx; scanf("%d", &n); init(); for(int i = 0; i < n; ++i) { scanf("%s %s %d", s[i][0], s[i][1], &limit[i]); hh = (s[i][0][0]-'0')*10+(s[i][0][1]-'0'); mm = (s[i][0][3]-'0')*10+(s[i][0][4]-'0'); tim[i][0] = hh*60+mm; hh = (s[i][1][0]-'0')*10+(s[i][1][1]-'0'); mm = (s[i][1][3]-'0')*10+(s[i][1][4]-'0'); tim[i][1] = hh*60+mm; } for(int i = 0; i < n; ++i) for(int j = i+1; j < n; ++j) //根据题目把冲突抽象出来,然后建边 { minn = min(tim[i][0], tim[j][0]); maxx = max(tim[i][0]+limit[i], tim[j][0]+limit[j]); if(maxx-minn < limit[i]+limit[j]) { add(i*2, j*2+1); add(j*2, i*2+1); } minn = min(tim[i][0], tim[j][1]-limit[j]); maxx = max(tim[i][0]+limit[i], tim[j][1]); if(maxx-minn < limit[i]+limit[j]) { add(i*2, j*2); add(j*2+1, i*2+1); } minn = min(tim[i][1]-limit[i], tim[j][1]-limit[j]); maxx = max(tim[i][1], tim[j][1]); if(maxx-minn < limit[i]+limit[j]) { add(i*2+1, j*2); add(j*2+1, i*2); } minn = min(tim[i][1]-limit[i], tim[j][0]); maxx = max(tim[i][1], tim[j][0]+limit[j]); if(maxx-minn < limit[i]+limit[j]) { add(i*2+1, j*2+1); add(j*2, i*2); } } } int dfs(int cur) //进行dfs的目的是为了把所有的后代节点都染为红色 { if(mark[cur^1]) return 0; //它的矛盾节点已经染成红色了，则方案不可行 if(mark[cur]) return 1; //记忆化搜索优化，已经染成红色，意味着其所有后代节点也已被染成红色 mark[cur] = 1; S[++top] = cur; //存储此次尝试标记所有点，失败则回退 int k = head[cur]; while(k != -1) { if(!dfs(edge[k].v)) return 0; k = edge[k].next; } return 1; } void print() { for(int i = 0; i < n; ++i) { if(mark[i*2] == 1) { int mm = tim[i][0]+limit[i]; printf("%s %02d:%02d\n", s[i][0], mm/60, mm%60); } if(mark[i*2+1] == 1) { int mm = tim[i][1]-limit[i]; printf("%02d:%02d %s\n", mm/60, mm%60, s[i][1]); } } } void solve() { for(int i = 0; i < n*2; i+=2) { if(mark[i] || mark[i+1]) continue; //只有当前集合内两个元素都未被染色才可进行选择染色 top = 0; if(!dfs(i)) //第一个染色失败 { while(top) mark[S[top--]] = 0; //反悔 if(!dfs(i+1)) //一个集合中两个元素都不能被选择染色，则无解 { puts("NO"); return; } } } puts("YES"); print(); } int main() { mapping(); //建边构图 solve(); return 0; }

继续加油~

参考博文:

http://blog.csdn.net/jarjingx/article/details/

http://www.cnblogs.com/-ZZB-/p/6635483.html

http://www.cnblogs.com/cnblogs321114287/p/4284360.html

http://www.cnblogs.com/acSzz/archive/2012/09/05/2672472.html