LOJ_Explosion.cpp

#include<bits/stdc++.h>
using namespace std;

#define dbg(a)  cerr << __LINE__ << ": " << #a << " = " << a << '\n'

struct graph
{
    int n, cnt;
    vector<vector<int>> g, gt;
    vector<int> vis, cno, assignment;   //cno: component number of i
    stack <int> st;

    graph(int n): n(n), g(n), gt(n){}

    void add_edge(int u, int v){
        g[u].emplace_back(v);
        gt[v].emplace_back(u);
    }

    void remove_edge(int u, int v){
        g[u].pop_back();
        gt[v].pop_back();
    }

    void dfs1(int v){
        vis[v] = 1;
        for(int u: g[v]){
            if(!vis[u])
                dfs1(u);
        }
        st.push(v);
    }

    void dfs2(int v){
        cno[v]=cnt;
        for(int u: gt[v])
            if(cno[u]==-1)
                dfs2(u);
    }


    bool sat(){
        vis.assign(n, 0);
        for (int i = 0; i < n; ++i){
            if(!vis[i])
                dfs1(i);
        }

        cno.assign(n, -1);
        cnt=0;
        while (!st.empty()){
            int u=st.top(); st.pop();
            if(cno[u]==-1){
                dfs2(u);
                cnt++;
            }
        }

        assignment.clear();
        for (int i = 0; i < n; i+=2){
            if(cno[i]==cno[i+1]){
                return false;
            }
            if(cno[i]>cno[i+1]){
                assignment.emplace_back(i/2+1);
            }
        }
        return true;
    }

    vector<int> getAssignment(){
        return assignment;
    }
};

int main(){
    int T, tc = 0;
    scanf("%d", &T);
    while(T--){
        printf("Case %d: ", ++tc);
        int n, m, k;    scanf("%d %d %d", &n, &m, &k);
        graph g(2*n);
        for (int i = 0; i < m; ++i){
            int tp, u, v;   scanf("%d %d %d",&tp, &u, &v);
            u=2*--u;
            v=2*--v;
            if(tp==1){
                g.add_edge(u^1, v);
                g.add_edge(v^1, u);
            }
            else if(tp==2){
                g.add_edge(u^1, v^1);
                g.add_edge(v, u);
            }
            else if(tp==3){
                g.add_edge(u, v^1);
                g.add_edge(v, u^1);
            }
            else{
                g.add_edge(u^1, v);
                g.add_edge(v^1, u);
                g.add_edge(u, v^1);
                g.add_edge(v, u^1);
            }
        }
        int mem[k][4];
        for (int i = 0; i < k; ++i){
            scanf("%d %d %d %d", &mem[i][0], &mem[i][1], &mem[i][2], &mem[i][3]);
        }
        bool psbl = true;
        for (int i = 0; i < k; ++i){
            psbl = false;
            if(mem[i][0]==1){
                for (int j = 1; j < 4; ++j){
                    int u=mem[i][j];
                    u=2*--u;
                    g.add_edge(u^1, u);
                    if(g.sat()){
                        psbl = true;
                        // g.remove_edge(u^1, u);   //since it is valid, we shouldn't remove it
                        break;
                    }
                    g.remove_edge(u^1, u);
                }
            }
            else{
                for (int j = 1; j < 4; ++j){
                    int u=mem[i][j];
                    u=2*--u;
                    g.add_edge(u, u^1);
                    if(g.sat()){
                        psbl=true;
                        // g.remove_edge(u, u^1);   //since it is valid, we shouldn't remove it
                        break;
                    }
                    g.remove_edge(u, u^1);
                }
            }
            if(!psbl)   break;
        }
        if(!psbl)   printf("Impossible.\n");
        else{
            printf("Possible");
            vector<int> ans = g.getAssignment();
            printf(" %d", (int)ans.size());
            for(int u : ans)
                printf(" %d", u);
            printf(".\n");
        }
    }
    return 0;
}

/*
messages:
type:1------ a or b = a'->b and b'->a
type:2------ a or b' = a'->b' and b->a
type:3------ a' or b' = a->b' and b->a'
type:4------ a xor b = a'->b and b'->a and a->b' and b->a'

opinion:
type:1------ a or a = a'->a
type:2------ a' or a' = a->a'
*/