2-SAT solver

twosat.py

def DFS(v, visited, graph):
    "Depth-first search through graph, appending current node when returning"
    if visited[v]:
        return []
    visited[v] = True
    output = []
    for w in graph[v]:
        output += DFS(w, visited, graph)
    output.append(v)
    return output

def BuildComponents(v, C, visited, reverseGraph):
    "Build components from reverseGraph"
    if visited[v]:
        return C
    visited[v] = True
    if -v in C:
        raise Exception()
    if v not in C:
        C[v] = True
    for w in reverseGraph[v]:
        BuildComponents(w, C, visited, reverseGraph)
    return C

def TwoSAT(Q, n):
    """Calculate 2SAT for query Q with n variables.

    Returns None if no solution, else an object with variable index as key and
    boolean as value."""
    graph = []
    reverseGraph = []
    for i in range((n+1)*2):
        graph.append([])
        reverseGraph.append([])
    for (a, b) in Q:
        graph[-a].append(b)
        graph[-b].append(a)
        reverseGraph[a].append(-b)
        reverseGraph[b].append(-a)
    visited = [False] * ((n+1)*2)
    order = []
    for i in range(n):
        order += DFS(i+1, visited, graph)
        order += DFS(-(i+1), visited, graph)
    order = order[::-1]
    visited = [False] * ((n+1)*2)
    components = []
    try:
        for v in order:
            components.append(BuildComponents(v, {}, visited, reverseGraph))
    except:
        return
    values = {}
    while len(values) < n:
        c = components.pop()
        for p in c:
            if abs(p) not in values:
                values[abs(p)] = abs(p) == p
    return values

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