POJ 3678 – Katu Puzzle [2-SAT入门题]

Link

传送门

Problem

Katu Puzzle is presented as a directed graph G(V, E) with each edge e(a, b) labeled by a boolean operator op (one of AND, OR, XOR) and an integer c (0 ≤ c ≤ 1). One Katu is solvable if one can find each vertex Vi a value Xi (0 ≤ Xi ≤ 1) such that for each edge e(a, b) labeled by op and c, the following formula holds: XaopXb = c

Mean

有N个变量(01值),M个条件。每个条件形如:XaopXb = c,op为与非异或中的一种。问你是否有一种解满足M个条件。

Analysis

2-SAT模板题,根据输入的类型加入条件即可。注意addClause(int x, int xval, int y, int yval)为“x为xval或者y为yval”。

Code

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

const int maxn = 1024;

struct TwoSAT {
    int n, c, S[maxn*2];
    vector<int> G[maxn*2];
    bool mark[maxn*2];

    void init(int n) {
        this->n = n;
        for(int i = 0; i < n * 2; ++i)
            G[i].clear();
        memset(mark, 0, sizeof(mark));
    }
    bool dfs(int u) {
        if(mark[u ^ 1]) return false;
        if(mark[u]) return true;
        mark[u] = true;
        S[c++] = u;
        for(int i = 0; i < G[u].size(); ++i)
            if(!dfs(G[u][i])) return false;
        return true;
    }
    void addClause(int x, int xval, int y, int yval) {
        x = x * 2 + xval;
        y = y * 2 + yval;
        G[x^1].push_back(y);
        G[y^1].push_back(x);
    }
    bool solve() {
        for(int i = 0; i < n * 2; 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;
    }
}sat;



int main() {
    int N, M; scanf("%d%d", &N, &M);
    int a, b, c; char op[10];
    sat.init(N);
    while(M--) {
        scanf("%d%d%d%s", &a, &b, &c, op);
        if(op[0] == 'A') {
            if(c == 1) {
                sat.addClause(a, 1, b, 1);
                sat.addClause(a, 0, b, 1);
                sat.addClause(a, 1, b, 0);
            } else if(c == 0) {
                sat.addClause(a, 0, b, 0);
            }
        } else if(op[0] == 'O') {
            if(c == 1) {
                sat.addClause(a, 1, b, 1);
            } else if(c == 0) {
                sat.addClause(a, 0, b, 0);
                sat.addClause(a, 1, b, 0);
                sat.addClause(a, 0, b, 1);
            }
        } else if(op[0] == 'X') {
            if(c == 1) {
                sat.addClause(a, 1, b, 1);
                sat.addClause(a, 0, b, 0);
            } else if(c == 0) {
                sat.addClause(a, 1, b, 0);
                sat.addClause(a, 0, b, 1);
            }
        }
    }
    puts(sat.solve() ? "YES" : "NO");
    return 0;
}

欢迎留言