Cod sursa(job #2049584)

Utilizator retrogradLucian Bicsi retrograd Data 27 octombrie 2017 13:52:34
Problema 2SAT Scor 100
Compilator cpp Status done
Runda Arhiva educationala Marime 2.81 kb
#include <bits/stdc++.h>

using namespace std;

/**
 * Author: Emil Lenngren, Simon Lindholm
 * Date: 2011-11-29
 * Source:
 * Description: Calculates a valid assignment to boolean variables a, b, c,... to a 2-SAT problem, so that an expression of the type $(a\|\|b)\&\&(!a\|\|c)\&\&(d\|\|!b)\&\&...$ becomes true, or reports that it is unsatisfiable.
 * Negated variables are represented by bit-inversions (\texttt{\tilde{}x}).
 * Usage:
 *  TwoSat ts(number of boolean variables);
 *  ts.either(0, \tilde3); // Var 0 is true or var 3 is false
 *  ts.set_value(2); // Var 2 is true
 *  ts.at_most_one({0,\tilde1,2}); // <= 1 of vars 0, \tilde1 and 2 are true
 *  ts.solve(); // Returns true iff it is solvable
 *  ts.values[0..N-1] holds the assigned values to the vars
 * Time: O(N+E), where N is the number of boolean variables, and E is the number of clauses.
 */

struct TwoSat {
	int n;
	vector<vector<int>> G;
	vector<int> values; // 0 = false, 1 = true

	TwoSat(int n = 0) : n(n), G(2*n) {}

	int AddVar() { // (optional)
		G.emplace_back();
		G.emplace_back();
		return n++;
	}
    
    void Implies(int a, int b) {
		a = (a >= 0 ? 2*a : -1-2*a);
		b = (b >= 0 ? 2*b : -1-2*b);
        G[a].push_back(b);
    }
	void Either(int a, int b) {
		Implies(~a, b);
        Implies(~b, a);
	}
	void SetValue(int x) { Either(x, x); }

	void AtMostOne(const vector<int>& vals) { // (optional)
		if (vals.size() <= 1) return;
		int cur = ~vals[0];
		for (int i = 2; i < (int)vals.size(); ++i) {
			int nxt = AddVar();
			Either(cur, ~vals[i]);
			Either(cur, nxt);
			Either(~vals[i], nxt);
			cur = ~nxt;
		}
		Either(cur, ~vals[1]);
	}

    vector<int> enter, comp, stk;
    int timer = 0;
	int dfs(int node) {
		int low = enter[node] = ++timer, x; 
        stk.push_back(node);
		
        for (auto vec : G[node]) if (!comp[vec])
			low = min(low, enter[vec] ?: dfs(vec));
		++timer;
		if (low == enter[node]) do {
			x = stk.back(); stk.pop_back();
			comp[x] = timer;
			if (values[x >> 1] == -1)
				values[x >> 1] = 1 - x & 1;
		} while (x != node);
		return enter[node] = low;
	}

	bool Solve() {
		values.assign(n, -1);
		enter.assign(2 * n, 0); comp = enter;
		for (int i = 0; i < 2 * n; ++i) { 
            if (!comp[i])
                dfs(i);
        }
		for (int i = 0; i < n; ++i) {
            if (comp[2 * i] == comp[2 * i + 1])
                return false;
        }
        return true;
	}
};

int main() {
    ifstream cin("2sat.in");
    ofstream cout("2sat.out");

    int n, m; cin >> n >> m;
    TwoSat sat(n);
    for (int i = 0; i < m; ++i) {
        int a, b; cin >> a >> b;
        a = (a > 0 ? a - 1 : ~(-(a + 1)));
        b = (b > 0 ? b - 1 : ~(-(b + 1)));
        sat.Either(a, b);
    }
    if (sat.Solve() == false) cout << -1 << endl;
    else {
        for (auto x : sat.values)
            cout << x << " ";
        cout << endl;
    }
}