1def two_sat(num_vars, clauses):
2    # Variables are 1..num_vars. Literal encoding:
3    #  i  -> variable i
4    # -i  -> negation of variable i
5
6    def idx(lit):
7        v = abs(lit) - 1
8        return 2 * v + (0 if lit > 0 else 1)
9
10    def neg(i):
11        return i ^ 1
12
13    n = 2 * num_vars
14    g = [[] for _ in range(n)]
15    rg = [[] for _ in range(n)]
16
17    def add_edge(u, v):
18        g[u].append(v)
19        rg[v].append(u)
20
21    for a, b in clauses:
22        ai, bi = idx(a), idx(b)
23        add_edge(neg(ai), bi)
24        add_edge(neg(bi), ai)
25
26    order = []
27    seen = [False] * n
28
29    def dfs1(u):
30        seen[u] = True
31        for v in g[u]:
32            if not seen[v]:
33                dfs1(v)
34        order.append(u)
35
36    for i in range(n):
37        if not seen[i]:
38            dfs1(i)
39
40    comp = [-1] * n
41
42    def dfs2(u, c):
43        comp[u] = c
44        for v in rg[u]:
45            if comp[v] == -1:
46                dfs2(v, c)
47
48    c = 0
49    for u in reversed(order):
50        if comp[u] == -1:
51            dfs2(u, c)
52            c += 1
53
54    assignment = [False] * (num_vars + 1)
55    for var in range(1, num_vars + 1):
56        t = idx(var)
57        f = idx(-var)
58        if comp[t] == comp[f]:
59            return False, None
60        assignment[var] = comp[t] > comp[f]
61
62    return True, assignment[1:]
63
64
65ok, values = two_sat(
66    3,
67    [
68        (1, -2),   # (x1 v ~x2)
69        (-1, 3),   # (~x1 v x3)
70        (2, -3),   # (x2 v ~x3)
71    ],
72)
73print(ok, values)