POJ 3678 解题报告

这道题还是2-SAT的问题。一个variable只能取true或者false, 也就是说a 和 ~a（用a + N记录）只能选取一个。给一个他们之间逻辑操作的结果后，问在这些限制下能不能有可能的取法（对所有的a，取a还是~a）。

因为这道题还是不要求求出解法，而只是判断，所以和之前做过的POJ 3207是一样的，都算是“简单”的2-SAT问题。做法也是一样的，都是对a, a + N ..., b, b + N这些节点之间构图，然后用tarjan或者别的算法求最大强连通图。最后看是否存在一个节点a, a 和 a + N都取上了。这种情况下就存在conflict。因为在限制下，两者都必须同时取，而两者表示的是截然相反的变量（即非此即彼）。

但是这道题在3207之后做的，仍然卡了很久。还是因为对2-SAT的解法还是了解得不够深。

首先抛开这道题，记录下在POJ上遇到WA而不知道原因的时候怎么办，假定此时我们已经看过很多遍程序，都看着没有问题。

首先，在dicuss或者usaco的竞赛题目是能找到测试数据的。这种情况下相对容易，虽然如果只是在很大的测试数据下才WA也挺麻烦的（需要缩小测试数据缩小范围）。

其次，如果找不到测试数据，比如本题。就需要自己创造测试数据了。这道题我是用python遍历四个变量分别取0,1的情况（2**4=16），然后改变AND, OR, XOR的结果。对比我的程序和已知正确程序的结果。这样就找到了我错的测试数据，测试数据的规模还很小（n=m=4）。对我比较有用的两个测试数据：

4 4

0 1 0 XOR

1 2 0 AND

3 2 0 XOR

3 0 0 OR

答案： YES

4 4

0 1 1 XOR

1 2 1 AND

3 2 1 XOR

3 0 1 OR

答案：NO

回到这道题，在建图方面，我与看到的解法不一样。我创造了两个点0和1，分别表示false和true。因为有些情况下，我们能知道一个变量是true还是false。比如a AND b = 1，那么a和b都必须是true。这是需要在1和a,b之间建立双向边，在0和a + n, b + n之间建立双向边。

需要思考的情况是a && b = 0。此时a和b中有一个必须为false。即如果a为true,那么b必须为false（b的情况相同，需要同样处理。这里略去）。如何保证这一点，显然从a和b+n之间必须要有一条有向边。但是我们希望的结果是如果a和1在一个连通分量里面，b+n必须也在里面。显然，a -> b + n只一条有向边是不够的。解决方法是再加一条b + n到1的有向边。这样如果我们有1 <-> a （因为他们在同一个联通分量里面），因为我们还有a -> b + n -> 1，我们有1 <-> b +
n。这样b + n必然也在1所在的连通分量里面。

我没有理解看到的大部分解法的构图，个人觉得我的做法是我比较容易理解的构图。

thestoryofsnow

3678

Accepted

456K

141MS

C++

5134B

/*
ID: thestor1
LANG: C++
TASK: poj3678
*/
#include <iostream>
#include <fstream>
#include <cmath>
#include <cstdio>
#include <cstring>
#include <limits>
#include <string>
#include <vector>
#include <list>
#include <set>
#include <map>
#include <queue>
#include <stack>
#include <algorithm>
#include <cassert>

using namespace std;

// const int MAXN = 1000;
// const int MAXM = 1000000;

bool isundefined(int u, vector<int> &indexes)
{
return indexes[u] < 0;
}

void strongconnect(int u, int &index, vector<int> &indexes, vector<int> &lowlinks, int &SCCNO, vector<int> &sccnos, stack<int> &S, vector<bool> &onStack, const vector<vector<int> > &adjs)
{
// Set the depth index for u to the smallest unused index
indexes[u] = index;
lowlinks[u] = index;
index++;

S.push(u);
onStack[u] = true;

// Consider successors of u
for (int i = 0; i < adjs[u].size(); ++i)
{
int v = adjs[u][i];
if (isundefined(v, indexes))
{
// Successor v has not yet been visited; recurse on it
strongconnect(v, index, indexes, lowlinks, SCCNO, sccnos, S, onStack, adjs);
lowlinks[u] = min(lowlinks[u], lowlinks[v]);
}
else if (onStack[v])
{
// Successor v is in stack S and hence in the current SCC
lowlinks[u] = min(lowlinks[u], lowlinks[v]);
}
}

// If u is a root node, pop the stack and generate an SCC
if (indexes[u] == lowlinks[u])
{
// start a new strongly connected component
while (true)
{
int v = S.top();
S.pop();
onStack[v] = false;

// add v to current strongly connected component
sccnos[v] = SCCNO;

if (v == u)
{
break;
}
}

SCCNO++;
}
}

// Tarjan's strongly connected components algorithm
// See http://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm void tarjan(const int N, const vector<vector<int> > &adjs, int &SCCNO, vector<int> &sccnos)
{
int index = 0;
vector<int> indexes(N, -1);

vector<int> lowlinks(N, -1);

stack<int> S;
vector<bool> onStack(N, false);

for (int u = 0; u < N; ++u)
{
if (isundefined(u, indexes))
{
strongconnect(u, index, indexes, lowlinks, SCCNO, sccnos, S, onStack, adjs);
}
}
}

int main()
{
int N, M;
scanf("%d%d", &N, &M);

// in the 2-SAT sense, if i is x, then i + n is ~x
// adjs[0] refers to false and adjs[1] refers to true
vector<vector<int> > adjs(2 * N + 1 + 1, std::vector<int>());

int a, b, c;
char op[5]; // AND, OR, XOR
for (int i = 0; i < M; ++i)
{
scanf("%d%d%d%s", &a, &b, &c, op);
// printf("a: %d, b: %d, c: %d, op: [%s]\n", a, b, c, op);

// AND
if (op[0] == 'A')
{
if (c == 1)
{
// a && b = 1
// both a and b are true
// both ~a and ~b are false
adjs[1].push_back(a + 2);
adjs[1].push_back(b + 2);
adjs[a + 2].push_back(1);
adjs[b + 2].push_back(1);

adjs[0].push_back(a + 2 + N);
adjs[0].push_back(b + 2 + N);
adjs[a + 2 + N].push_back(0);
adjs[b + 2 + N].push_back(0);
}
else
{
// a && b = 0
// a is false or b is false
// if a is true then b is false (~b is true)
adjs[a + 2].push_back(b + 2 + N);
adjs[b + 2].push_back(a + 2 + N);
adjs[a + N + 2].push_back(1);
adjs[b + N + 2].push_back(1);
}
}
// OR
else if (op[0] == 'O')
{
if (c == 1)
{
// a || b = 1
// a is true or b is true
// if a is false then b is true
adjs[a + 2 + N].push_back(b + 2);
adjs[b + 2 + N].push_back(a + 2);
adjs[a + 2].push_back(1);
adjs[b + 2].push_back(1);
}
else
{
// a || b = 0
// both a and b are false
// a is false
// ~a is true
adjs[0].push_back(a + 2);
adjs[0].push_back(b + 2);
adjs[a + 2].push_back(0);
adjs[b + 2].push_back(0);

adjs[1].push_back(a + 2 + N);
adjs[1].push_back(b + 2 + N);
adjs[a + 2 + N].push_back(1);
adjs[b + 2 + N].push_back(1);
}
}
// XOR
else
{
if (c == 1)
{
// a ^ b = 1
// a is true then b is false
// a is false then b is true
adjs[a + 2].push_back(b + 2 + N);
adjs[b + 2].push_back(a + 2 + N);
adjs[a + 2 + N].push_back(b + 2);
adjs[b + 2 + N].push_back(a + 2);
}
else
{
// a ^ b = 0
// a is true then b is true
// a is false then b is false
adjs[a + 2].push_back(b + 2);
adjs[b + 2].push_back(a + 2);
adjs[a + 2 + N].push_back(b + 2 + N);
adjs[b + 2 + N].push_back(a + 2 + N);
}
}
}

// printf("[debug]adjs:\n");
// for (int i = 0; i < 2 * N + 1 + 1; ++i)
// {
// 	printf("%d: ", i);
// 	for (int j = 0; j < adjs[i].size(); ++j)
// 	{
// 		printf("%d ", adjs[i][j]);
// 	}
// 	printf("\n");
// }

int SCCNO = 0;
vector<int> sccnos(2 * N + 1 + 1, -1);
tarjan(2 * N + 1 + 1, adjs, SCCNO, sccnos);

// printf("[debug]sccnos[%d]:\n", SCCNO);
// for (int i = 0; i < 2 * N + 1 + 1; ++i)
// {
// 	printf("%d: %d\n", i, sccnos[i]);
// }

bool conflict = (sccnos[0] == sccnos[1]);
for (int i = 2; i <= N + 1; ++i)
{
// if both x and ~x are true, we have conflicts here
if (sccnos[i] == sccnos[i + N])
{
conflict = true;
break;
}
}

if (conflict)
{
printf("NO\n");
}
else
{
printf("YES\n");
}
return 0;
}