hdoj 3062 Party(2-SAT)

题目链接：http://acm.hdu.edu.cn/showproblem.php?pid=3062

思路分析：将问题转换为2-SAT问题，需要注意的是将命题转换为有向图的方法；命题中A1, A2, C1, C2表示C1与C2不能同时出现，所以A1中C1出现等价于A2中C2 ^ 1出现，同理A2中C2出现等价于A1中C1^1出现，则形成了两条有向边；

代码如下：

#include <cstdio>
#include <vector>
#include <cstring>
#include <iostream>
using namespace std;

const int MAX_N = 1000 + 10;
struct TwoSAT {
    int n;
    vector<int> G[2 * MAX_N];
    bool mark[2 * MAX_N];
    int S[2 * MAX_N], c;

    void Init(int n)
    {
        this->n = n;
        for (int i = 0; i <= 2 * n; ++i)
            G[i].clear();
        memset(mark, 0, sizeof(mark));
    }

    bool Dfs(int x)
    {
        if (mark[x ^ 1])  return false;
        if (mark[x])      return true;
        mark[x] = true;
        S[c++] = x;

        for (int i = 0; i < G[x].size(); ++i)
        if (!Dfs(G[x][i]))
            return false;
        return true;
    }

    void AddClause(int x, int x_val, int y, int y_val)
    {
        x = 2 * x + x_val;
        y = 2 * y + y_val;
        G[x].push_back(y ^ 1);
        G[y].push_back(x ^ 1);
    }

    bool Solve()
    {
        for (int i = 0; i < 2 * n; i += 2)
        {
            if (!mark[i] && !mark[i + 1])
            {
                c = 0;
                if (!Dfs(i))
                {
                    while (c > 0) mark[S[--c]] = false;
                    if (!Dfs(i + 1))  return false;
                }
            }
        }
        return true;
    }
};

TwoSAT sat;

int main()
{
    int n, m;

    while (scanf("%d", &n) != EOF)
    {
        scanf("%d", &m);
        sat.Init(n);
        for (int i = 0; i < m; ++i)
        {
            int x, x_val, y, y_val;
            scanf("%d %d %d %d", &x, &y, &x_val, &y_val);
            sat.AddClause(x, x_val, y, y_val);
        }
        bool ans = sat.Solve();
        if (ans)
            printf("YES
");
        else
            printf("NO
");
    }
    return 0;
}