2-SAT

INCLUDE

• Graph::ImplicationGraph ➝ /cp/graph/implication-graph

Note

You can also add additional constraints using more clauses:

1. Forcing a variable (say $x$) to be true: $(x\vee x)$
2. Exactly one variable must be true: $(x\vee y)\wedge (\neg x\vee \neg y)$
3. At least one variable must be true: $(x\vee y)$
4. Both variables must have the same value: $(\neg x\vee y)\wedge (x\vee \neg y)$

Code

constexpr int N = 1'000'005;
Graph::ImplicationGraph<N> ig;

inline void solve() {
    int n, m; cin >> n >> m;
    ig.set(n);
    for (int i = 0; i < m; ++i) {
        // add clause (x v y) which is same as (~x => y)
        int x, y; bool x_negated, y_negated;
        cin >> x >> x_negated >> y >> y_negated;
        x_negated ^= 1;
        ig.addClause((x << 1) | x_negated, (y << 1) | y_negated);
    }

    vector<int> solution = ig.solve();
    for (int i = 1; i <= n; ++i) {
        cout << solution[i] << ' ';
    }
    cout << endl;
}