#!/usr/bin/env python3

#------------------------------------------
# data structures
#------------------------------------------

class Node:
    def __init__(self, data):
        self.data = data
        self.in_degree = 0
        self.out_degree = 0
        
        # used during DFS
        self.isMarked = False
        self.pre = 0
        self.post = 0

    def __str__(self):
        return str(self.data)

class DirectGraph:
    def __init__(self, table=None, is_tree=False, root=None):
        self.table = table if table else {}
        self.isTree = is_tree
        self.root = root

        if root is not None:
            self.insert_node(root)

    @staticmethod
    def create_tree(root):
        tree = DirectGraph(is_tree=True, root=root)
        return tree

    def insert_node(self, node):
        if node not in self.table:
            self.table[node] = []

    def insert_arc(self, u, v):
        if u in self.table and v in self.table:
            u.out_degree += 1
            v.in_degree += 1
            self.table[u].append(v)

    def __str__(self):
        graph_str = "{"

        for u in self.table:
            graph_str += str(u) + ": ["

            line = ""
            for v in self.table[u]:
                line += str(v) + ", "

            graph_str += line[:-2] + "], "

        graph_str = graph_str[:-2] + "}\n"
        return graph_str

#------------------------------------------
# graph algorithms
#------------------------------------------

# reverses the direction of the links in the input graph to produce
# the output graph.
def reverse_graph(graph):
    r_graph = DirectGraph()

    for u in graph.table:
        r_graph.insert_node(u)

    for u in graph.table:
        for v in graph.table[u]:
            # If graph had the arc (u, v), then r_graph has (v, u) as
            # the corresponding arc
            r_graph.insert_arc(v, u)

    return r_graph

# computes a topological order of the graph given as input.
def topological_order(graph):
    sources = []
    nodes = []
    in_degree = {}

    for u in graph.table:
        in_degree[u] = u.in_degree
        if u.in_degree == 0:
            sources.append(u)

    while sources:
        u = sources.pop()
        nodes.append(u)

        for v in graph.table[u]:
            in_degree[v] -= 1
            if in_degree[v] == 0:
                sources.append(v)

    # the graph contained a cycle and therefore a topological order
    # could not be computed.
    if len(nodes) != len(graph.table.keys()):
        return None

    return nodes


clock = 0

def depth_first_search_rec(graph, u, visit_tree=None, visited_nodes=None):
    global clock

    u.isMarked = True
    u.pre = clock
    clock += 1

    for v in graph.table[u]:
        if not v.isMarked:

            if visit_tree is not None:
                visit_tree.insert_node(v)
                visit_tree.insert_arc(u, v)

            depth_first_search_rec(graph, v, visit_tree, visited_nodes)

    u.post = clock
    if visited_nodes is not None:
        visited_nodes.insert(0, u)
    clock += 1

# This function performs a local dfs (depth first search) by visiting
# only the portion of the graph that is reachable starting from node
# u.
def local_dfs(graph, u):
    global clock
    clock = 1

    for u in graph.table:
        u.isMarked = False

    visit_tree = DirectGraph.create_tree(u)
    visited_nodes = []
    depth_first_search_rec(graph, u, visit_tree=visit_tree, visited_nodes=visited_nodes)
    return visit_tree, visited_nodes

# This functions performs a global dfs (depth first search) by visiting
# all of the graph. 
def global_dfs(graph):
    global clock
    clock = 1

    for u in graph.table:
        u.isMarked = False

    # NOTE: visited_nodes contains a list of nodes ordered by
    # decreasing values of post(v). This means that the first node in
    # visited_nodes will be the last node visited, and the last node
    # will be the first node visited.
    forest = []
    visited_nodes = []

    for v in graph.table:
        if not v.isMarked:
            visit_tree = DirectGraph.create_tree(v)
            depth_first_search_rec(graph, v, visit_tree, visited_nodes)
            forest.append(visit_tree)
            
    return forest, visited_nodes

# returns the graph of the connected components of the graph given in
# input
def connected_components_graph(graph):
    forest, visited_nodes = global_dfs(graph)
    
    node2comp = {}
    for i in range(0, len(forest)):
        for u in forest[i].table.keys():
            node2comp[u] = i

    comp_len = len(forest)
    comp_graph = DirectGraph()
    number2node = {}
    nodes_in_component = [[] for _ in range(0, comp_len)]

    # each node in comp_graph corresponds to a connected component.
    for i in range(0, comp_len):
        number2node[i] = Node(i)
        comp_graph.insert_node(number2node[i])

    # add edges between different components in comp_graph
    for u in graph.table:
        for v in graph.table[u]:
            if node2comp[u] != node2comp[v]:
                comp_graph.insert_arc(number2node[node2comp[u]], number2node[node2comp[v]])

        nodes_in_component[node2comp[u]].append(u)

    return comp_graph, nodes_in_component

#------------------------------------------
# main section
#------------------------------------------

def implication_graph(formula, n):
    """
    Construct the implication graph of the formula given as input.

    :param formula: [(int, int)] boolean formula.
    :param n: int number of variables.

    :return: <dict> implication graph of the formula.
    """

    table = {}
    number_node = {}

    # Construct V
    for i in range(1, n + 1):
        number_node[i] = Node(i)
        number_node[-i] = Node(-i)

        table[number_node[i]] = []
        table[number_node[-i]] = []

    # Construct E
    for clause in formula:
        (i, j) = clause
        table[number_node[-i]].append(number_node[j])
        table[number_node[-j]].append(number_node[i])

    return DirectGraph(table)

def sat_2(formula, n):
    graph = implication_graph(formula, n)
    graph_comp, nodes_in_components = connected_components_graph(graph)

    # If in a given component there is both a literate value and its
    # opposite, then the formula cannot be satisfiable, and therefore
    # None can be returned.
    for component in nodes_in_components:
        nodes_seen = {}
        for node in component:
            if (-node.data) in nodes_seen:
                return None
            else:
                nodes_seen[node.data] = True

    # initialize truth assignment
    truth_assignment = [None for i in range(1, n+2)]
    
    # construct truth assignment
    t_sort = topological_order(graph_comp)    
    while t_sort:
        last_comp = t_sort.pop()

        for node in nodes_in_components[last_comp.data]:
            var = node.data
            # Can I assign it's truth valued or have I already done that?
            if var > 0 and truth_assignment[var] is None:
                truth_assignment[var] = True
            elif var < 0 and truth_assignment[-var] is None:
                truth_assignment[-var] = False                

    return truth_assignment[1:]

if __name__ == "__main__":
    f = [(1, 2), (-1, -2), (2, -3)]
    t = sat_2(f, 3)
    print(t)