from collections import defaultdict
import matplotlib.pyplot as plt

# 1-SAT Lahendaja
def solve_1sat_problem(clauses):
    assignment = set()
    for clause in clauses:
        if -clause in assignment:
            return []  # Konflikt leitud, lahendust ei eksisteeri
        assignment.add(clause)
    return list(assignment)

# Tarjani algoritm SCC-de jaoks
def tarjan_scc(graph, n):
    index = 0
    indices = [-1] * (2 * n + 1)
    lowlink = [-1] * (2 * n + 1)
    on_stack = [False] * (2 * n + 1)
    stack = []
    sccs = []

    def strong_connect(v):
        nonlocal index
        indices[v] = index
        lowlink[v] = index
        index += 1
        stack.append(v)
        on_stack[v] = True

        for w in graph[v]:
            if indices[w] == -1:
                strong_connect(w)
                lowlink[v] = min(lowlink[v], lowlink[w])
            elif on_stack[w]:
                lowlink[v] = min(lowlink[v], indices[w])

        if lowlink[v] == indices[v]:
            scc = []
            while True:
                w = stack.pop()
                on_stack[w] = False
                scc.append(w)
                if w == v:
                    break
            sccs.append(scc)

    for v in range(-n, n + 1):
        if v != 0 and indices[v] == -1:
            strong_connect(v)

    return sccs

# 2-SAT Lahendaja
def solve_2sat_problem(clauses):
    n = max(abs(literal) for clause in clauses for literal in clause)
    graph = defaultdict(list)

    def add_implication(u, v):
        graph[-u].append(v)
        graph[-v].append(u)

    for u, v in clauses:
        add_implication(u, v)

    sccs = tarjan_scc(graph, n)
    assignment = [-1] * (n + 1)
    scc_index = {v: i for i, scc in enumerate(sccs) for v in scc}

    for i in range(1, n + 1):
        if scc_index[i] == scc_index[-i]:
            return []  # Lahendust ei eksisteeri
        assignment[i] = scc_index[-i] > scc_index[i]

    return [i if assignment[i] else -i for i in range(1, n + 1)]

# 3-SAT Lahendaja koos Kihistamisega
def solve_3sat_problem(clauses):
    n = max(abs(literal) for clause in clauses for literal in clause)
    graph = defaultdict(list)

    def add_implication(u, v, w):
        graph[-u].append(v)
        graph[-v].append(w)
        graph[-w].append(u)

    for u, v, w in clauses:
        add_implication(u, v, w)

    sccs = tarjan_scc(graph, n)
    assignment = [-1] * (n + 1)
    scc_index = {v: i for i, scc in enumerate(sccs) for v in scc}

    for i in range(1, n + 1):
        if scc_index[i] == scc_index[-i]:
            return []  # Lahendust ei eksisteeri
        assignment[i] = scc_index[-i] > scc_index[i]

    return [i if assignment[i] else -i for i in range(1, n + 1)]

# Visualiseerimisfunktsioon 2-SAT lahenduste jaoks
def visualize_2sat_solution(clauses, solution, is_valid):
    fig, ax = plt.subplots(figsize=(10, 8))
    ax.set_title(f"2-SAT Probleemi Lahendus\nKehtiv: {is_valid}")
    ax.set_xlabel("Klauslid")
    ax.set_ylabel("Literaalide Arv")

    sample_size = min(50, len(clauses))
    sample_clauses = clauses[:sample_size]

    literals = [literal for clause in sample_clauses for literal in clause]
    counts = defaultdict(int)
    for literal in literals:
        counts[literal] += 1

    literals, occurrences = zip(*sorted(counts.items()))

    ax.bar(literals, occurrences)
    plt.show()

# 2-SAT lahenduse valideerimine
def validate_2sat_solution(clauses, solution):
    if not solution:
        return False

    assignment = {abs(lit): (lit > 0) for lit in solution}

    for u, v in clauses:
        if (u > 0 and not assignment[abs(u)]) and (v > 0 and not assignment[abs(v)]):
            return False
        if (u < 0 and assignment[abs(u)]) and (v < 0 and assignment[abs(v)]):
            return False

    return True

# 3-SAT lahenduse valideerimine (hüpoteetiline, ainult illustreerimiseks)
def validate_3sat_solution(clauses, solution):
    if not solution:
        return False

    assignment = {abs(lit): (lit > 0) for lit in solution}

    for u, v, w in clauses:
        if not ((assignment[abs(u)] if u > 0 else not assignment[abs(u)]) or
                (assignment[abs(v)] if v > 0 else not assignment[abs(v)]) or
                (assignment[abs(w)] if w > 0 else not assignment[abs(w)])):
            return False

    return True

# 3-SAT klauslite kihistamine
def layer_clauses_3sat(clauses):
    layers = defaultdict(list)
    for clause in clauses:
        layer_key = abs(clause[0])
        layers[layer_key].append(clause)
    return layers

# Näide 3-SAT kasutusest koos kihistamisega
clauses_3sat = [
    (1, -2, 3), (-1, 2, -3), (2, 3, -4), (-2, -3, 4),
    (4, -5, 6), (-4, 5, -6), (5, 6, -7), (-5, -6, 7)
]

layers = layer_clauses_3sat(clauses_3sat)

for layer in layers:
    print(f"Layer {layer}:")
    solution_3sat_layered = solve_3sat_problem(layers[layer])
    is_valid_3sat_layered = validate_3sat_solution(layers[layer], solution_3sat_layered)
    print(f"3-SAT Solution for Layer {layer}:", solution_3sat_layered)
    print(f"Is the 3-SAT solution valid for Layer {layer}?", is_valid_3sat_layered)
    print()

# Näide 1-SAT kasutusest
clauses_1sat = [1, -2, 3, 4, -5, 6, -7, 8, 9, -10, 11, -12]
solution_1sat = solve_1sat_problem(clauses_1sat)
print("1-SAT Solution:", solution_1sat)

# Näide 2-SAT kasutusest
clauses_2sat = [
    (1, -2), (2, 3), (-3, 4), (-1, -4), (5, -6), (-5, 7), (6, -7), (8, -9),
    (-8, 10), (9, -10), (11, 12), (-11, -12), (13, -14), (-13, 14), (-15, 16),
    (15, -16), (17, -18), (-17, 18), (19, -20), (-19, 20), (21, -22), (-21, 22),
    (23, -24), (-23, 24), (25, -26), (-25, 26), (27, -28), (-27, 28), (29, -30),
    (-29, 30), (31, -32), (-31, 32), (33, -34), (-33, 34), (35, -36), (-35, 36),
    (37, -38), (-37, 38), (39, -40), (-39, 40), (41, -42), (-41, 42), (43, -44),
    (-43, 44), (45, -46), (-45, 46), (47, -48), (-47, 48), (49, -50), (-49, 50)
]
solution_2sat = solve_2sat_problem(clauses_2sat)
print("2-SAT Solution:", solution_2sat)

# 2-SAT lahenduse valideerimine ja visualiseerimine
is_valid_2sat = validate_2sat_solution(clauses_2sat, solution_2sat)
print("Is the 2-SAT solution valid?", is_valid_2sat)
visualize_2sat_solution(clauses_2sat, solution_2sat, is_valid_2sat)

# Hüpoteetiline 3-SAT kasutus koos kihistamisega
clauses_3sat = [
    (1, -2, 3), (-1, 2, -3), (2, 3, -4), (-2, -3, 4),
    (4, -5, 6), (-4, 5, -6), (5, 6, -7), (-5, -6, 7),
    (8, -9, 10), (-8, 9, -10), (9, 10, -11), (-9, -10, 11),
    (12, -13, 14), (-12, 13, -14), (13, 14, -15), (-13, -14, 15)
]

layers = layer_clauses_3sat(clauses_3sat)

for layer in layers:
    print(f"Layer {layer}:")
    solution_3sat_layered = solve_3sat_problem(layers[layer])
    is_valid_3sat_layered = validate_3sat_solution(layers[layer], solution_3sat_layered)
    print(f"3-SAT Solution for Layer {layer}:", solution_3sat_layered)
    print(f"Is the 3-SAT solution valid for Layer {layer}?", is_valid_3sat_layered)
    visualize_3sat_solution(layers[layer], solution_3sat_layered, is_valid_3sat_layered)
    print()

# Näide 3-SAT lahenduse visualiseerimisest (valikuline)
def visualize_3sat_solution(clauses, solution, is_valid):
    fig, ax = plt.subplots(figsize=(10, 8))
    ax.set_title(f"3-SAT Probleemi Lahendus\nKehtiv: {is_valid}")
    ax.set_xlabel("Klauslid")
    ax.set_ylabel("Literaalide Arv")

    sample_size = min(50, len(clauses))
    sample_clauses = clauses[:sample_size]

    literals = [literal for clause in sample_clauses for literal in clause]
    counts = defaultdict(int)
    for literal in literals:
        counts[literal] += 1

    literals, occurrences = zip(*sorted(counts.items()))

    ax.bar(literals, occurrences)
    plt.show()

# 3-SAT lahenduse valideerimine ja visualiseerimine iga kihi jaoks
for layer in layers:
    solution_3sat_layered = solve_3sat_problem(layers[layer])
    is_valid_3sat_layered = validate_3sat_solution(layers[layer], solution_3sat_layered)
    print(f"3-SAT Solution for Layer {layer}:", solution_3sat_layered)
    print(f"Is the 3-SAT solution valid for Layer {layer}?", is_valid_3sat_layered)
    visualize_3sat_solution(layers[layer], solution_3sat_layered, is_valid_3sat_layered)
    print()