2-SAT

1
#include <bits/stdc++.h>
2
using namespace std;
3
4
struct TwoSAT {
5
    int n;                          // number of variables
6
    vector<vector<int>> g, gr;      // implication graph and its reverse
7
    vector<int> comp;               // component id per node
8
    vector<int> order;              // finish order in first pass
9
    vector<int> vis;                // visited flag
10
    vector<int> assignment;         // resulting assignment for variables
11
12
    explicit TwoSAT(int n_vars) : n(n_vars) {
13
        g.assign(2*n, {});
14
        gr.assign(2*n, {});
15
    }
16
17
    // Map (var, value) -> node id. value=true means literal x_var; value=false means literal ¬x_var
18
    static int id(int var, bool value) { return (var<<1) ^ (value ? 0 : 1); }
19
    static int neg(int x) { return x ^ 1; }  // complement literal index
20
21
    // Add implication u -> v
22
    void add_implication(int u, int v) {
23
        g[u].push_back(v);
24
        gr[v].push_back(u);
25
    }
26
27
    // Add clause (x_var=valueX) OR (y_var=valueY)
28
    void add_or(int x_var, bool valueX, int y_var, bool valueY) {
29
        int a = id(x_var, valueX);
30
        int b = id(y_var, valueY);
31
        add_implication(neg(a), b); // ¬a -> b
32
        add_implication(neg(b), a); // ¬b -> a
33
    }
34
35
    // Force literal (v=value) to be true
36
    void add_true(int v, bool value) {
37
        int a = id(v, value);
38
        add_implication(neg(a), a); // (a) ≡ (¬a -> a)
39
    }
40
41
    // Add implication (x=valueX) -> (y=valueY)
42
    void add_implies(int x_var, bool valueX, int y_var, bool valueY) {
43
        int a = id(x_var, valueX);
44
        int b = id(y_var, valueY);
45
        add_implication(a, b);
46
    }
47
48
    // Add equivalence (x == y)
49
    void add_equiv(int x, bool vx, int y, bool vy) {
50
        add_implies(x, vx, y, vy);
51
        add_implies(y, vy, x, vx);
52
    }
53
54
    // Add XOR: exactly one of (x=vx) or (y=vy)
55
    void add_xor(int x, bool vx, int y, bool vy) {
56
        // (x=vx OR y=vy) AND (¬(x=vx) OR ¬(y=vy))
57
        add_or(x, vx, y, vy);
58
        add_or(x, !vx, y, !vy);
59
    }
60
61
    // Add at-most-one among provided literals (pairwise O(k^2) clauses)
62
    void add_at_most_one(const vector<pair<int,bool>>& lits) {
63
        int k = (int)lits.size();
64
        for (int i = 0; i < k; ++i) for (int j = i+1; j < k; ++j) {
65
            int a = id(lits[i].first,  lits[i].second);
66
            int b = id(lits[j].first,  lits[j].second);
67
            // not both true: (¬a OR ¬b)
68
            add_or(a>>1, !( (a&1)==0 ), b>>1, !( (b&1)==0 ));
69
            // The above expands to add_implication(a, neg(b)) and add_implication(b, neg(a))
70
        }
71
    }
72
73
    // First pass DFS to compute finishing order (recursive for clarity)
74
    void dfs1(int v) {
75
        vis[v] = 1;
76
        for (int to : g[v]) if (!vis[to]) dfs1(to);
77
        order.push_back(v);
78
    }
79
80
    // Second pass DFS on reversed graph to assign components
81
    void dfs2(int v, int cid) {
82
        comp[v] = cid;
83
        for (int to : gr[v]) if (comp[to] == -1) dfs2(to, cid);
84
    }
85
86
    bool solve() {
87
        int N = 2*n;
88
        vis.assign(N, 0);
89
        order.clear(); order.reserve(N);
90
        for (int v = 0; v < N; ++v) if (!vis[v]) dfs1(v);
91
        comp.assign(N, -1);
92
        int cid = 0;
93
        for (int i = N-1; i >= 0; --i) {
94
            int v = order[i];
95
            if (comp[v] == -1) {
96
                dfs2(v, cid++);
97
            }
98
        }
99
        assignment.assign(n, 0);
100
        for (int i = 0; i < n; ++i) {
101
            if (comp[2*i] == comp[2*i^1]) return false; // x and ¬x in same SCC -> UNSAT
102
            assignment[i] = (comp[2*i] > comp[2*i^1]);  // later component set to true
103
        }
104
        return true;
105
    }
106
};
107
108
int main() {
109
    ios::sync_with_stdio(false);
110
    cin.tie(nullptr);
111
112
    // Example: variables x0, x1, x2
113
    // Constraints:
114
    // (x0 OR x1), (¬x0 OR x2), (¬x1 OR ¬x2), and x2 -> x0
115
    TwoSAT sat(3);
116
    sat.add_or(0, true, 1, true);      // x0 ∨ x1
117
    sat.add_or(0, false, 2, true);     // ¬x0 ∨ x2
118
    sat.add_or(1, false, 2, false);    // ¬x1 ∨ ¬x2
119
    sat.add_implies(2, true, 0, true); // x2 -> x0
120
121
    bool ok = sat.solve();
122
    if (!ok) {
123
        cout << "UNSATISFIABLE\n";
124
    } else {
125
        cout << "SATISFIABLE\nAssignment:" << '\n';
126
        for (int i = 0; i < 3; ++i) cout << "x" << i << " = " << (sat.assignment[i] ? "true" : "false") << '\n';
127
    }
128
    return 0;
129
}
130

1
#include <bits/stdc++.h>
2
using namespace std;
3
4
// Reuse the TwoSAT structure from the previous example (implemented inline here for a standalone file)
5
struct TwoSAT {
6
    int n; vector<vector<int>> g, gr; vector<int> comp, order, vis; vector<int> assignment;
7
    explicit TwoSAT(int n_vars): n(n_vars) { g.assign(2*n, {}); gr.assign(2*n, {}); }
8
    static int id(int var, bool val){ return (var<<1) ^ (val?0:1);} static int neg(int x){return x^1;}
9
    void add_implication(int u,int v){ g[u].push_back(v); gr[v].push_back(u);}    
10
    void add_or(int x,bool vx,int y,bool vy){ int a=id(x,vx), b=id(y,vy); add_implication(neg(a),b); add_implication(neg(b),a);}    
11
    void add_implies(int x,bool vx,int y,bool vy){ add_implication(id(x,vx), id(y,vy)); }
12
    void add_true(int x,bool vx){ int a=id(x,vx); add_implication(neg(a), a);}    
13
    void add_exactly_one(int x,int y){ // exactly one of x,y is true    
14
        add_or(x,true, y,true);      // at least one
15
        add_or(x,false,y,false);     // at most one
16
    }
17
    void dfs1(int v){ vis[v]=1; for(int to:g[v]) if(!vis[to]) dfs1(to); order.push_back(v);}    
18
    void dfs2(int v,int cid){ comp[v]=cid; for(int to:gr[v]) if(comp[to]==-1) dfs2(to,cid);}    
19
    bool solve(){ int N=2*n; vis.assign(N,0); order.clear(); order.reserve(N); for(int v=0;v<N;++v) if(!vis[v]) dfs1(v); comp.assign(N,-1); int cid=0; for(int i=N-1;i>=0;--i){ int v=order[i]; if(comp[v]==-1) dfs2(v,cid++);} assignment.assign(n,0); for(int i=0;i<n;++i){ if(comp[2*i]==comp[2*i^1]) return false; assignment[i]=(comp[2*i]>comp[2*i^1]); } return true; }
20
};
21
22
// Problem: We have tasks, each with two possible time slots. Some slots conflict with others.
23
// Model: For task i, variable i means "choose slot A"; then ¬i means "choose slot B".
24
// We want exactly one slot per task, and we ban conflicting pairs of chosen slots.
25
int main(){
26
    ios::sync_with_stdio(false); cin.tie(nullptr);
27
28
    int tasks = 4; // tasks 0..3
29
    TwoSAT sat(tasks);
30
31
    // Exactly one of two slots for each task i (A or B)
32
    for(int i=0;i<tasks;++i){
33
        // At least one: (slotA or slotB) = (i or ¬i) is always true; but we must enforce exactly one.
34
        // Exactly one for two choices reduces to XOR of (i) and (¬i): that is just setting a variable! Simpler:
35
        // Force that the variable takes some boolean value; no explicit clause needed.
36
        // However, to illustrate, we add (i ∨ ¬i) and (¬i ∨ i) which are tautologies; the real constraint is at most one:
37
        sat.add_or(i, true, i, false);  // tautology, kept for symmetry
38
        sat.add_or(i, false, i, true);  // tautology
39
        // At most one between slotA and slotB is (¬i ∨ ¬¬i) = (¬i ∨ i), also a tautology. For two options, "exactly one" is inherent:
40
        // choosing slot A corresponds to setting variable i=true; B means i=false. So there is exactly one by construction.
41
    }
42
43
    // Now encode conflicts between concrete slots:
44
    // Let's say task 0's slot A conflicts with task 1's slot A: (x0=true) and (x1=true) cannot both hold -> (¬x0 ∨ ¬x1)
45
    sat.add_or(0,false, 1,false); // which encodes "not both (0=true) and (1=true)" as (¬x0 ∨ ¬x1)
46
47
    // task 1's slot B conflicts with task 2's slot A
48
    // That means not( x1=false AND x2=true ) -> (x1=true OR ¬x2) i.e., (x1 ∨ ¬x2)
49
    sat.add_or(1,true, 2,false);
50
51
    // task 2's slot B conflicts with task 3's slot B
52
    // not( x2=false AND x3=false ) -> (x2=true OR x3=true)
53
    sat.add_or(2,true, 3,true);
54
55
    // Additionally, suppose choosing task 3's slot A implies task 0 must take slot B: (x3=true) -> (x0=false)
56
    sat.add_implies(3,true, 0,false);
57
58
    bool ok = sat.solve();
59
    if(!ok){ cout << "UNSATISFIABLE\n"; return 0; }
60
    cout << "SATISFIABLE\n";
61
    for(int i=0;i<tasks;++i){
62
        cout << "Task " << i << ": choose slot " << (sat.assignment[i] ? 'A' : 'B') << "\n";
63
    }
64
    return 0;
65
}
66

1
#include <bits/stdc++.h>
2
using namespace std;
3
4
struct TwoSATTarjan {
5
    int n, N;                                  // n variables, N = 2*n nodes
6
    vector<vector<int>> g;                     // implication graph
7
    vector<int> index_, low, comp, st;         // Tarjan arrays
8
    vector<char> onstack;                      // on-stack flags
9
    int timer = 0, comps = 0;                  // DFS index and component count
10
    vector<int> assignment;                    // result
11
12
    explicit TwoSATTarjan(int n_vars): n(n_vars), N(2*n_vars) {
13
        g.assign(N, {});
14
    }
15
16
    static int id(int var, bool val){ return (var<<1) ^ (val?0:1);}    
17
    static int neg(int x){ return x ^ 1; }
18
19
    void add_implication(int u, int v){ g[u].push_back(v); }
20
21
    // (x=vx) OR (y=vy)
22
    void add_or(int x,bool vx,int y,bool vy){ int a=id(x,vx), b=id(y,vy); add_implication(neg(a), b); add_implication(neg(b), a);}    
23
24
    // implication (x=vx) -> (y=vy)
25
    void add_implies(int x,bool vx,int y,bool vy){ add_implication(id(x,vx), id(y,vy)); }
26
27
    // equivalence (x == y)
28
    void add_equiv(int x,bool vx,int y,bool vy){ add_implies(x,vx,y,vy); add_implies(y,vy,x,vx); }
29
30
    // XOR exactly one of two literals true
31
    void add_xor(int x,bool vx,int y,bool vy){ add_or(x,vx,y,vy); add_or(x,!vx,y,!vy);}    
32
33
    void tarjan(int v){
34
        index_[v] = low[v] = ++timer;
35
        st.push_back(v); onstack[v] = 1;
36
        for(int to: g[v]){
37
            if(index_[to] == 0){ tarjan(to); low[v] = min(low[v], low[to]); }
38
            else if(onstack[to]) low[v] = min(low[v], index_[to]);
39
        }
40
        if(low[v] == index_[v]){
41
            // root of an SCC
42
            while(true){
43
                int w = st.back(); st.pop_back(); onstack[w] = 0;
44
                comp[w] = comps;
45
                if(w == v) break;
46
            }
47
            ++comps;
48
        }
49
    }
50
51
    bool solve(){
52
        index_.assign(N, 0); low.assign(N, 0); comp.assign(N, -1); onstack.assign(N, 0); st.clear(); timer = 0; comps = 0;
53
        for(int v=0; v<N; ++v) if(index_[v]==0) tarjan(v);
54
        assignment.assign(n, 0);
55
        for(int i=0;i<n;++i){ if(comp[2*i] == comp[2*i^1]) return false; assignment[i] = (comp[2*i] > comp[2*i^1]); }
56
        return true;
57
    }
58
};
59
60
int main(){
61
    ios::sync_with_stdio(false); cin.tie(nullptr);
62
63
    // Build two scenarios: one SAT, one UNSAT
64
    {
65
        cout << "Scenario 1 (SAT)\n";
66
        TwoSATTarjan sat(3);
67
        // x0 -> x1 ; x1 <-> x2 ; x0 XOR x2
68
        sat.add_implies(0,true, 1,true);      // x0 -> x1
69
        sat.add_equiv(1,true, 2,true);        // x1 == x2
70
        sat.add_xor(0,true, 2,true);          // x0 XOR x2
71
        bool ok = sat.solve();
72
        if(!ok){ cout << "UNSATISFIABLE\n"; }
73
        else{ cout << "SATISFIABLE\n"; for(int i=0;i<3;++i) cout << "x"<<i<<"="<<(sat.assignment[i]?"T":"F")<<" "; cout << "\n"; }
74
    }
75
76
    {
77
        cout << "\nScenario 2 (UNSAT)\n";
78
        TwoSATTarjan sat(2);
79
        // Force contradiction on x0: x0 -> ¬x0 and ¬x0 -> x0
80
        sat.add_implies(0,true, 0,false);
81
        sat.add_implies(0,false, 0,true);
82
        // Also add unrelated clauses with x1
83
        sat.add_or(1,true, 1,false);  // tautology
84
        bool ok = sat.solve();
85
        if(!ok) cout << "UNSATISFIABLE (x0 and ¬x0 in same SCC)\n";
86
        else{ cout << "SATISFIABLE (unexpected)\n"; }
87
    }
88
    return 0;
89
}
90