def two_sat(formula):
    #                                   -- n est le nombre de variables
    n = max(abs(clause[p]) for p in (0, 1) for clause in formula)
    graph = [[] for node in range(2 * n)]
    for x, y in formula:                           # x or y
        graph[_vertex(-x)].append(_vertex(y))      # -x => y
        graph[_vertex(-y)].append(_vertex(x))      # -y => x
    sccp = tarjan(graph)
    comp_id = [None] * (2 * n)           # pour chaque nœud l'id. de sa comp.
    affectations = [None] * (2 * n)
    for component in sccp:
        rep = min(component)             # représentation de la composante
        for vtx in component:
            comp_id[vtx] = rep
            if affectations[vtx] == None:
                affectations[vtx] = True
                affectations[vtx ^ 1] = False    # littéral complémentaire
    for i in range(n):
        if comp_id[2 * i] == comp_id[2 * i + 1]:
            return None                          # formule insatisfiable
    return affectations[::2]
# snip}
Solving a 2-SAT boolean formula
dataset/ETHPy150Open jilljenn/tryalgo/tryalgo/two_sat.py/two_sat