import random
from collections import defaultdict
import matplotlib.pyplot as plt
from concurrent.futures import ThreadPoolExecutor

# Tarjan's algorithm for finding SCCs
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

# 3-SAT Solver with Layering
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 []  # No solution exists
        assignment[i] = scc_index[-i] > scc_index[i]

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

# Visualization function for 3-SAT solutions
def visualize_3sat_solution(clauses, solution, is_valid):
    fig, ax = plt.subplots(figsize=(10, 8))
    ax.set_title(f"3-SAT Problem Solution\nValid: {is_valid}")
    ax.set_xlabel("Clauses")
    ax.set_ylabel("Number of Literals")

    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 solution validation
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

# Generate random 3-SAT problem
def generate_random_3sat(num_variables, num_clauses):
    clauses = []
    for _ in range(num_clauses):
        clause = tuple(random.sample([random.choice([-1, 1]) * i for i in range(1, num_variables + 1)], 3))
        clauses.append(clause)
    return clauses

# Split clauses into layers
def split_into_layers(clauses, num_layers):
    layers = [[] for _ in range(num_layers)]
    for i, clause in enumerate(clauses):
        layers[i % num_layers].append(clause)
    return layers

# Solve and validate each layer in parallel
def process_layer(layer):
    solution = solve_3sat_problem(layer)
    is_valid = validate_3sat_solution(layer, solution)
    return solution, is_valid

# Translate solution to clauses
def translate_solution_to_clauses(solution, num_variables):
    clauses = []
    for lit in solution:
        a = lit
        b = random.choice([i for i in range(1, num_variables + 1) if i != abs(a)]) * random.choice([-1, 1])
        c = random.choice([i for i in range(1, num_variables + 1) if i != abs(a) and i != abs(b)]) * random.choice([-1, 1])
        clause = (a, b, c)
        clauses.append(clause)
    return clauses

# Example usage
num_variables = 10
num_clauses = 30
num_layers = 10
clauses = generate_random_3sat(num_variables, num_clauses)
layers = split_into_layers(clauses, num_layers)

with ThreadPoolExecutor(max_workers=num_layers) as executor:
    futures = [executor.submit(process_layer, layer) for layer in layers]
    results = [future.result() for future in futures]

overall_valid_count = 0

for i, (solution, is_valid) in enumerate(results):
    print(f"Layer {i+1} Solution:", solution)
    print(f"Is the solution valid for Layer {i+1}?", is_valid)
    visualize_3sat_solution(layers[i], solution, is_valid)
    translated_clauses = translate_solution_to_clauses(solution, num_variables)
    print(f"Translated Clauses for Layer {i+1}:", translated_clauses)
    overall_valid_count += is_valid
    print()

# Calculate precision
precision = overall_valid_count / num_layers * 100
print(f"Overall Precision: {precision}%")