Pagini recente » Cod sursa (job #2499490) | Cod sursa (job #2143770) | Cod sursa (job #2043351) | Cod sursa (job #459219) | Cod sursa (job #2049584)
#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;
}
}