2-sat专辑
2012-04-07 15:29
169 查看
一、关于模型:
一个2-SAT模型应该是一个满足以下的条件的满足性问题:
1、该模型中存在2n个可以分成n组的元素,每组两个元素。
2、每组元素中,选择了其中一个元素,另外一个元素就不能被选择。这两个元素记为a和!a。
3、该模型中的元素之间存在一些关系,且这些关系是对称的。(除非是同一组元素中的关系,这些关系限定了“必须选择”该组中的某一个元素,可能单独出现)
满足上述条件,要求在满足给定关系的情况下在每组元素中选出一个元素的问题称为2-SAT问题。问是否存在即2-SAT判定问题,当然也可以求出一组可行解。
当你看见一道题目,一些事物只有唯一且互斥的两种选择(比如两种取值,两种连接方式等等),那么可以分析下题目给出的条件是否满足对称性,若满足则可通过构图将题目转化成2-SAT问题了。
二、关于构图
要解2-SAT问题或者完成判定问题,首要的任务是构图。从《由对称性解2-SAT问题》这篇论文里,我们可以知道,构图的关键是找到冲突。
1.不能同时选择X和Y,那么就X—->partner[Y]、Y—->partner[X]。
2.至少有X、Y其中的一个,经过德摩根定律,相当于不能同时选择partner[X]和partner[Y]。
3.必须选择X:partner[X]—->X(不能选择X就反过来)
三、关于解2-SAT
对原图求一次强连通分量,然后看每组中的两个点是否属于同一个强连通分量,如果存在这种情况,那么无解。
一个2-SAT模型应该是一个满足以下的条件的满足性问题:
1、该模型中存在2n个可以分成n组的元素,每组两个元素。
2、每组元素中,选择了其中一个元素,另外一个元素就不能被选择。这两个元素记为a和!a。
3、该模型中的元素之间存在一些关系,且这些关系是对称的。(除非是同一组元素中的关系,这些关系限定了“必须选择”该组中的某一个元素,可能单独出现)
满足上述条件,要求在满足给定关系的情况下在每组元素中选出一个元素的问题称为2-SAT问题。问是否存在即2-SAT判定问题,当然也可以求出一组可行解。
当你看见一道题目,一些事物只有唯一且互斥的两种选择(比如两种取值,两种连接方式等等),那么可以分析下题目给出的条件是否满足对称性,若满足则可通过构图将题目转化成2-SAT问题了。
二、关于构图
要解2-SAT问题或者完成判定问题,首要的任务是构图。从《由对称性解2-SAT问题》这篇论文里,我们可以知道,构图的关键是找到冲突。
1.不能同时选择X和Y,那么就X—->partner[Y]、Y—->partner[X]。
2.至少有X、Y其中的一个,经过德摩根定律,相当于不能同时选择partner[X]和partner[Y]。
3.必须选择X:partner[X]—->X(不能选择X就反过来)
三、关于解2-SAT
对原图求一次强连通分量,然后看每组中的两个点是否属于同一个强连通分量,如果存在这种情况,那么无解。
public class SAT { class node { int be, ne; node(int be, int ne) { this.be = be; this.ne = ne; } } int E[], n, cnt, index; node buf[]; int len, top; int dfn[], low[], stack[], id[];// 0~cnt-1 boolean instack[]; int sccout[], num[]; SAT(int maxn, int maxm) { E = new int[maxn]; buf = new node[maxm]; dfn = new int[maxn]; low = new int[maxn]; stack = new int[maxn]; id = new int[maxn]; instack = new boolean[maxn]; num = new int[maxn]; satinit(maxn); } void init(int n) { this.n = n; Arrays.fill(E, -1); len = 0; } void add(int a, int b) { buf[len] = new node(b, E[a]); E[a] = len++; } void dfs(int a) { dfn[a] = low[a] = ++index; instack[a] = true; stack[top++] = a; int b = -1; for (int i = E[a]; i != -1; i = buf[i].ne) { b = buf[i].be; if (dfn[b] == 0) { dfs(b); if (low[b] < low[a]) low[a] = low[b]; } else if (instack[b] && dfn[b] < low[a]) low[a] = dfn[b]; } if (low[a] == dfn[a]) { do { b = stack[--top]; instack[b] = false; id[b] = cnt; num[cnt]++; } while (b != a); cnt++; } } void solve() { // 求强连通分量 index = top = 0; cnt = 0; Arrays.fill(dfn, 0); Arrays.fill(low, 0); Arrays.fill(num, 0); Arrays.fill(instack, false); for (int i = 0; i < n; i++) if (dfn[i] == 0) dfs(i); } int Escc[], partner[];//同组点在哪个连通分量中 node bufscc[];//强连通逆向图 int lenscc, dgr[];//逆向图边数 各点入度 int color[];//各个强连通颜色 void satinit(int maxn) {// 初始化2sat Escc = new int[maxn]; partner = new int[maxn]; bufscc = new node[maxn * 5]; dgr = new int[maxn]; color = new int[maxn]; } boolean sat() { for (int i = 0; i < n / 2; i++) // i与i+n同组 if (id[i] == id[i + n / 2]) return false; for (int i = 0; i < n / 2; i++) {// 找出伙伴 partner[id[i]] = id[i + n / 2]; partner[id[i + n / 2]] = id[i]; } Arrays.fill(Escc, -1); lenscc = 0; Arrays.fill(dgr, 0); Arrays.fill(color, 0); for (int i = 0; i < n; i++) // 构造逆向缩点图i->b~b->i for (int j = E[i]; j != -1; j = buf[j].ne) { int b = buf[j].be; if (id[i] != id[b]) { bufscc[lenscc] = new node(id[i], Escc[id[b]]); Escc[id[b]] = lenscc++; dgr[id[i]]++; } } for (int i = 0; i < cnt; i++) if (dgr[i] == 0) stack[++top] = i; while (top != 0) { int now = stack[top--]; if (color[now] == 0) { color[now] = 1;// 红色,可行 color[partner[now]] = -1;// 蓝色 ,不可行 } for (int i = Escc[now]; i != -1; i = bufscc[i].ne) { int b = bufscc[i].be; if (--dgr[b] == 0) stack[++top] = b; } } return true; } void output() { for (int i = 0; i < n / 2; i++) { if (color[id[i]] == 1) System.out.println(i); else System.out.println(i + n / 2); } } }
相关文章推荐
- 风潮唱片-远方的寂静;专辑
- Now That's What I Call Music 16张专辑目录
- Aselin Debison 专辑收藏之 "Bigger Than Me" by Emerald 绿色学院 - green institute
- 电视原声专辑《The 4400》
- 养鹿专辑二:恋鹿篇之枕着老婆的梦编程
- 百首经典老歌新唱 [9张专辑]
- Asp.net Ajax Control Toolkit设计编程备忘录(色眼窥观版)——第1回(柿子专辑)
- 【博主推荐】linux-电子书下载专辑
- 专辑《原创音乐王》歌曲洪森《不想明天说再见》
- 分享一张不错听的专辑//Better Now Than Never//
- 2-SAT问题
- 2009-12-12 Sat
- android 如何将imageCursor.getColumnIndex(MediaStore.Audio.AlbumColumns.ALBUM_KEY)中的到的专辑封面放入view中显示
- Google Music专辑下载工具,喜欢用Google Music可以看看
- 唱响艾泽拉斯-Zetacola专辑
- 【DP专辑】ACM动态规划总结
- hdu 3622 Bomb Game 继续2-sat
- 2-SAT——3.0(poj3207)
- poj 2723【2-SAT+二分】
- 【转】2-SAT问题及其算法