资深光能
RT
资深光能
初始2-SAT那时还是在研一时上了一门叫做计算复杂性的课，教材是一本英文的书，很难。当时，第一次接触了不可判定的问题，疯狂地看了很多东西。又系统地学习了复杂度类P,NP(C)，受益颇多。3-SAT就是NPC了，而2-SAT确是P的。
所谓2-SAT就是2元可满足性问题。首先，作为众所周知的，任何布尔表达式，都可以化为合取范式的形式，即化为： () and () and () ...and () 其中括号里面的是用析取符号or 连接的变量或者变量的非的形式。我们一般称，变量或者变量的非为“文字”,而括号里的叫做子句。可满足性问题是要给所有的变量一个赋值（真或假）使得表达式值为真。而2元可满足性问题，就是化为合取范式后，每个子句最多有两个文字的可满足性问题。
cook定理已经说明，一般地可满足性问题是NPC的。但是值得注意的是，2-SAT却是P的。简单分析一下2-SAT: 它要求每个子句的值都是真。考虑一个子句，a or b ，显然如果a取false，则b一定取true，反之亦然。先给出算法：
假设2-SAT问题中有N个变量，则构造一个有向图包含2n个节点。每个节点代表一个变量或者变量的非（即代表一个文字）。对每个子句a or b,在途中加2条有向边 (~a,b)和(~b,a) (其中~表示变量的非)。然后对这个有向图求强连通分量，把每个强连通分量看作一个点（缩点），这样新的有向图是无环的（无环有向图又叫DAG）。如果一个强连通分量里同时包含了同一个变量以及它的非，则原问题是不可满足的。否则，我们可以构造解，对这个DAG可以进行拓扑排序，按照节点的拓扑排序顺序的倒序进行如下操作：找到此顺序中第一个没有标记的节点，把此节点标记成true，并且把和此节点矛盾的节点（一个节点包含了a，另外一个节点包含了~a，则称它们是矛盾的），以及祖先标记成false，直到所有节点都有标记，结束。这些标记也对应着变量的取值。
大概不严谨地证明一下，首先同一个强连通分量里的文字是等价的。因为对一个子句a or b，按照一个取假，另外一个一定取真的意思，连的边表示逻辑中的“蕴含”关系，即有~a->b ，~b->a。这样一个强连通分量里的文字互相蕴含，所以是等价的。于是，当存在a->~a->a时，显然原问题不可满足。
第二，因为每标记一个true，立刻把与它矛盾的并且“反向蕴含”的点都设置为false，所以，这样的赋值不会产生矛盾。
第三，不会把一个变量和它的非都设置为false。
这是因为，考虑设置变量为false时，假设设置a为true，沿着“反向蕴含链”把x设置为false了，这说明有x->~a,由于对称性，有a->~x （这里的->表示有路相连，并不一定是一条边），按照算法流程必须要先考虑~x （拓扑排序的逆序），可见这时~x应该已经被设置为true了，因为否则的话，如果~x=false，则会沿着“反向蕴含链”把a也设置为false的，根本不会到考虑a为true的这一步骤了。于是，设置false是安全的。
综上所述，该算法可以找到一组2-SAT的可行解，或者判断无解。该算法的复杂度：求强连通分量、拓扑排序、以及遍历图都是O(m)的，其中m是边数。
从网上找了段2-SAT的C++类的代码，修改了一下：
#include
#include
#include
#include
using namespace std;
const int N = 5050; //最大人数
const int inf=6000001;
class SAT
{
private:
vector g[N]; //原图边连接情况
int n, M, h[N], id[N]; //id[]表示原图中每个点都属于哪个强连通分量
int cnt, scnt, dfn[N], low[N], cur[N];
int stack[N], top, est[N], etop;
vector tree[N]; //有向无环图的边连接情况(新图)
vector contain[N]; //新图中每个点都包含原图中的哪些点
void dfs(int);
void tsDfs(int);
void topologicalSort();
void colorDfs(int);
void color();
void tagAnswer();
void printAnswer();
void getOneAnswer();
void buildGraph();
public:
void scR();
void build(int);
bool judge();
bool solve();
void make(int,int);
};
/*
函数build是对原图初始化(根据实际输入情况做相应的更改)
*/
void SAT::make(int x,int y) { // x || y 负数表示非 1<=|x| , |y| <=M 注意从1开始
int x1,x2,y1,y2;
if (x > 0) {
x1 = x - 1;
x2 = x1 + M;
}
else {
x2 = -x - 1;
x1 = x2 + M;
}
if (y > 0 ) {
y1 = y - 1;
y2 = y1 + M;
}
else {
y2 = -y - 1;
y1 = y2 + M;
}
g[x2].push_back(y1);
g[y2].push_back(x1);
}
void SAT::build(int num) //变量个数
{
int i;
M = num;
n = M << 1;
for (i = 0 ; i < n ; ++i) {
g[i].clear();
}
}
void SAT::dfs(int src)
{
etop = top = 0;
stack[top++] = src;
while(top != 0)
{
int c = stack[top-1];
if(dfn[c] == -1)
{
h[c] = dfn[c] = low[c] = cnt++;
est[etop++] = c;
}
for(; cur[c] >= 0; cur[c]--)
{
int no = g[c][cur[c]];
if(dfn[no] == -1)
{
stack[top++] = no;
break;
}
if (h[c]>low[no]) {
h[c] = low[no];
}
}
if(cur[c] >= 0)
continue;
top--;
int k;
if(h[c] != low[c])
{
low[c] = h[c];
continue;
}
do
{
k = est[--etop];
id[k] = scnt; low[k] = N;
} while(k != c);
scnt++;
}
}
/*
函数scR和dfs是求原图的强连通分量(代码由wywcgs原创)
*/
void SAT::scR()
{
int i;
memset(dfn, 0xff, sizeof(dfn));
cnt = scnt = 0;
for(i = 0; i < n; i++)
{
cur[i] = g[i].size()-1;
contain[i].clear();
}
for(i = 0; i < n; i++)
if(dfn[i] == -1)
dfs(i);
/*
统计每个强连通分量都包含哪些点，为后面求可行方案做准备。如果不求可行解，可注释掉。
*/
for ( i=0;i
{
contain[id[i]].push_back(i);
}
}
/*
函数judge判断是否能找出一个可行方案出来
*/
bool SAT::judge()
{
int i;
for ( i=0;i
if (id[i]==id[i + M])
return false;
return true;
}
/*
函数buildGraph把每个强连通分量作为一个点，重新构图。(缩点，得到的是一个有向无环图)
用的是链接表的形式，可能有很多重边。可以加一些预处理消除重边。
*/
void SAT::buildGraph()
{
int i,j;
for (i=0;i
tree[i].clear();
for (i=0;i
for (j=0;j
{
int a=id[i];
int b=id[g[i][j]];
if (a!=b)
{
tree.push_back(a);
}
}
}
void SAT::tsDfs(int k)
{
dfn[k]=cnt++;
for (int i=0;i
{
int w=tree[k][i];
if (dfn[w]==-1)
{
tsDfs(w);
}
}
low[scnt++]=k;
}
/*
函数topologicalSort和tsDfs是对新图进行拓扑排序，排序后的结果存在low数组中
*/
void SAT::topologicalSort()
{
int i;
for ( i=0;i<scnt;i++)
{
dfn[i]=-1;
low[i]=-1;
}
int nn=scnt;
cnt=scnt=0;
for ( i=0;i<nn;i++)
{
if (dfn[i]==-1)
tsDfs(i);
}
}
/*
函数color和colorDfs是对新图进行着色，新图中着色为1的点组成一组可行解
*/
void SAT::color()
{
int i;
for ( i=0;i
dfn[i]=-1;
for ( i=scnt-1;i>=0;i--)
if (dfn[low[i]]==-1)
{
/*
新图中low[i]着色为1后，它的矛盾点应标记为2
*/
int a=contain[low[i]][0]; //在原图中找一点属于强连通分量low[i]的点a，点a所属组的另一点b所属的强连通分量id一定是low[i]矛盾点。
int b;
if (a >= M)
b= a - M;
else
b= a + M;
dfn[low[i]]=1;
if (dfn[id]==-1)
colorDfs(id); //由于依赖关系，有id能达的点都是low[i]的矛盾点
}
}
/*
函数tagAnswer由新图对原图的点进行标记，得到原图的可行解
*/
void SAT::tagAnswer()
{
int i,j;
for ( i=0;i
low[i]=-1;
for (i=0;i
if (dfn[i]==1)//i为新图中可行解包含的点，那么原图中强连通分量属于i的点都是原图中可行解的点
{
for ( j=0;j
low[contain[i][j]]=1;
}
}
/*
函数printAnswer打印原图的可行解
*/
void SAT::printAnswer() {
}
/*
函数getOneAnswer得到原图的一组可行解
*/
void SAT::getOneAnswer()
{
buildGraph();
topologicalSort();
color();
tagAnswer();
}
/*
函数solve可根据实际要求，进行更改输出 */
bool SAT::solve()
{
scR();
if (judge())
{
//puts("YES");
//getOneAnswer();
//printAnswer();
return true;
}
else {
// puts("NO");
return false;
}
}
用法： 先build(n) n是变量的个数，再通过make(i,j) 加入子句 xi or xj (负数表示变量取反 i,j是正整数 )
solve判断有无解，getOneAnswer得到一组赋值，printOneAnswer根据情况输出一组解
可优化的地方：可以用set存放临接表，进而去除重边。拓扑排序可以写成非递归的，而不用递归的dfs……
小技巧：
表示xor 关系的表达 如果要表示 a xor b = true 即 a b有且仅有一个为true 则可以表达为2个子句：
a or b 和 ~a or ~b
表示同或关系 即a xor b = false 即a=b 则可表达为两个子句：
~a or b 和 a or ~b
表示 a and b = true 即两个都是true
可以表达为2个子句 a or a 和b or b
表示 a and b = false 即至少有一个是false
可以表达为: ～a or ~b
表示 a or b = false 即全是false
可表达为 ~a or ~a和~b or ~b
表示 a为true时 b不能为false
可以表达为 ~a or b
……
作为acm算法的训练题：
http://acm.pku.edu.cn/JudgeOnline/problem?id=2723
http://acm.pku.edu.cn/JudgeOnline/problem?id=2749
http://acm.pku.edu.cn/JudgeOnline/problem?id=3207
http://acm.pku.edu.cn/JudgeOnline/problem?id=3648
http://acm.pku.edu.cn/JudgeOnline/problem?id=3678
http://acm.pku.edu.cn/JudgeOnline/problem?id=3683
资深光能
??
新手守护
高级天翼
呃呃
缔造者之神
1
