// 2-SAT con el grafo de implicaciones. Esta versión es recursiva y guarda todo en estructuras simples,
// porque aquí solo corre con fórmulas pequeñas. Con millones de nodos, la pila no alcanza: ahí va la
// pila explícita de la semana 6.
#pragma once
#include <cstddef>
#include <cstdlib>
#include <optional>
#include <utility>
#include <vector>
#include "cnf.h"

using TwoClause = std::pair<int, int>;

// El nodo de un literal: x_v es 2(v − 1), y ¬x_v es 2(v − 1) + 1.
inline std::size_t two_sat_node(int literal) {
    std::size_t v = static_cast<std::size_t>(std::abs(literal) - 1);
    return 2 * v + (literal > 0 ? 0 : 1);
}

inline int two_sat_literal(std::size_t node) {
    int v = static_cast<int>(node / 2) + 1;
    return node % 2 == 0 ? v : -v;
}

using ImplicationGraph = std::vector<std::vector<int>>;

// Cada cláusula (a ∨ b) da ¬a → b y ¬b → a. Con both = false sale la versión con una sola arista.
inline ImplicationGraph implication_graph(int variables, const std::vector<TwoClause>& clauses, bool both = true) {
    ImplicationGraph g(2 * static_cast<std::size_t>(variables));
    for (auto [a, b] : clauses) {
        g[two_sat_node(-a)].push_back(static_cast<int>(two_sat_node(b)));
        if (both) g[two_sat_node(-b)].push_back(static_cast<int>(two_sat_node(a)));
    }
    return g;
}

inline void finish_order_from(const ImplicationGraph& g, std::size_t u, std::vector<char>& seen, std::vector<std::size_t>& order) {
    seen[u] = 1;
    for (int v : g[u]) {
        if (!seen[static_cast<std::size_t>(v)]) finish_order_from(g, static_cast<std::size_t>(v), seen, order);
    }
    order.push_back(u);
}

inline void label_from(const ImplicationGraph& g, std::size_t u, int label, std::vector<int>& comp) {
    comp[u] = label;
    for (int v : g[u]) {
        if (comp[static_cast<std::size_t>(v)] == -1) label_from(g, static_cast<std::size_t>(v), label, comp);
    }
}

// Kosaraju-Sharir como en la semana 6: las componentes salen de sumidero a fuente, numeradas desde 0.
// Por eso una arista u → v entre componentes distintas cumple comp[u] > comp[v].
inline std::vector<int> implication_components(const ImplicationGraph& g) {
    ImplicationGraph inverted(g.size());
    for (std::size_t u = 0; u < g.size(); u++) {
        for (int v : g[u]) inverted[static_cast<std::size_t>(v)].push_back(static_cast<int>(u));
    }
    std::vector<char> seen(g.size(), 0);
    std::vector<std::size_t> order;
    for (std::size_t u = 0; u < g.size(); u++) {
        if (!seen[u]) finish_order_from(inverted, u, seen, order);
    }
    std::vector<int> comp(g.size(), -1);
    int label = 0;
    for (std::size_t i = order.size(); i-- > 0;) {
        if (comp[order[i]] == -1) label_from(g, order[i], label++, comp);
    }
    return comp;
}

inline bool same_component_clash(const std::vector<int>& comp) {
    for (std::size_t node = 0; node < comp.size(); node += 2) {
        if (comp[node] == comp[node + 1]) return true;
    }
    return false;
}

// x es verdadera si su componente salió antes que la de ¬x: está más cerca de los sumideros.
inline Assignment assignment_from_components(const std::vector<int>& comp) {
    Assignment a(comp.size() / 2 + 1, false);
    for (std::size_t v = 1; v < a.size(); v++) a[v] = comp[2 * (v - 1)] < comp[2 * (v - 1) + 1];
    return a;
}

// El error: leer el orden al revés.
inline Assignment assignment_with_reversed_order(const std::vector<int>& comp) {
    Assignment a(comp.size() / 2 + 1, false);
    for (std::size_t v = 1; v < a.size(); v++) a[v] = comp[2 * (v - 1)] > comp[2 * (v - 1) + 1];
    return a;
}

inline std::optional<Assignment> solve_two_sat(int variables, const std::vector<TwoClause>& clauses) {
    std::vector<int> comp = implication_components(implication_graph(variables, clauses));
    if (same_component_clash(comp)) return std::nullopt;
    return assignment_from_components(comp);
}

inline Formula two_clauses_as_formula(int variables, const std::vector<TwoClause>& clauses) {
    Formula f{variables, {}};
    for (auto [a, b] : clauses) f.clauses.push_back({a, b});
    return f;
}