// Las pruebas de lo que afirman los apuntes de la semana 14.
#include <algorithm>
#include <cassert>
#include <cstdint>
#include <iostream>
#include <random>
#include <vector>
#include "coloring.h"
#include "frontier.h"
#include "independent_set.h"
#include "knapsack_search.h"
#include "subset_sum.h"
#include "three_sat.h"
#include "two_sat.h"

namespace {

using Random = std::mt19937;

int below(Random& random, int limit) { return static_cast<int>(random() % static_cast<std::uint32_t>(limit)); }

// Fórmula en CNF con cláusulas de cualquier largo, con repetidos y con x ∨ ¬x.
Formula random_cnf(Random& random, int variables, int clauses, int longest) {
    Formula f{variables, {}};
    for (int c = 0; c < clauses; c++) {
        Clause clause;
        int size = 1 + below(random, longest);
        for (int i = 0; i < size; i++) {
            int v = 1 + below(random, variables);
            clause.push_back(below(random, 2) ? v : -v);
        }
        f.clauses.push_back(clause);
    }
    return f;
}

// Fórmula 3-SAT: tres variables distintas por cláusula.
Formula random_three(Random& random, int variables, int clauses) {
    Formula f{variables, {}};
    for (int c = 0; c < clauses; c++) {
        int a = 1 + below(random, variables);
        int b = a;
        int d = a;
        while (b == a) b = 1 + below(random, variables);
        while (d == a || d == b) d = 1 + below(random, variables);
        f.clauses.push_back({below(random, 2) ? a : -a, below(random, 2) ? b : -b, below(random, 2) ? d : -d});
    }
    return f;
}

Graph random_graph(Random& random, int n, int percent) {
    Graph g(static_cast<std::size_t>(n));
    for (int u = 0; u < n; u++) {
        for (int v = u + 1; v < n; v++) {
            if (below(random, 100) < percent) add_edge(g, u, v);
        }
    }
    return g;
}

void test_three_sat() {
    Random random(1401);
    for (int round = 0; round < 1500; round++) {
        Formula f = random_cnf(random, 1 + below(random, 5), below(random, 5), 7);
        Formula out = to_three_sat(f);
        // Forma: exactamente tres literales, de tres variables distintas.
        for (const Clause& c : out.clauses) {
            assert(c.size() == 3);
            assert(std::abs(c[0]) != std::abs(c[1]) && std::abs(c[0]) != std::abs(c[2]) && std::abs(c[1]) != std::abs(c[2]));
        }
        // Tamaño: k literales dan a lo sumo máx(k, 4) cláusulas nuevas y a lo sumo máx(k, 2) variables.
        std::size_t clause_bound = 0;
        int variable_bound = f.variables;
        for (const Clause& c : f.clauses) {
            clause_bound += std::max<std::size_t>(c.size(), 4);
            variable_bound += std::max(static_cast<int>(c.size()), 2);
        }
        assert(out.clauses.size() <= clause_bound);
        assert(out.variables <= variable_bound);
        // Las dos direcciones. La de ida es constructiva, y la de vuelta se lee restringiendo.
        auto sat = brute_sat(f);
        if (out.variables <= 14) {
            auto sat_out = brute_sat(out);
            assert(sat.has_value() == sat_out.has_value());
            if (sat_out) {
                Assignment restricted(sat_out->begin(), sat_out->begin() + f.variables + 1);
                assert(satisfies(f, restricted));
            }
        }
        if (sat) assert(satisfies(out, extend_assignment(f, *sat, out.variables)));
    }
    // Una cláusula vacía nunca se cumple, y su reemplazo tampoco.
    Formula empty{1, {{}}};
    assert(!brute_sat(empty));
    assert(!brute_sat(to_three_sat(empty)));
    // Una cláusula con x y ¬x desaparece.
    assert(to_three_sat({2, {{1, -1, 2}}}).clauses.empty());
}

void test_independent_set() {
    Random random(1402);
    for (int round = 0; round < 1500; round++) {
        Formula f = random_three(random, 3 + below(random, 3), 1 + below(random, 8));
        IndependentSetInstance s = reduce_to_independent_set(f);
        std::vector<int> best = max_independent_set(s.graph);
        auto sat = brute_sat(f);
        assert(is_independent(s.graph, best));
        assert(static_cast<int>(best.size()) <= s.k);  // a lo sumo uno por triángulo
        assert(sat.has_value() == (static_cast<int>(best.size()) == s.k));
        if (sat) {
            std::vector<int> nodes = set_from_assignment(f, *sat);
            assert(static_cast<int>(nodes.size()) == s.k && is_independent(s.graph, nodes));
            assert(satisfies(f, assignment_from_set(f, s, best)));
        }
    }
    // Pregunta de repaso 2.
    Formula two{3, {{1, -2, 3}, {-1, 2, -3}}};
    assert(max_independent_set(reduce_to_independent_set(two).graph).size() == 2);
    // Las ocho cláusulas: no hay solución, y falta justo uno. Sin alguna clase de aristas, la respuesta es falsa.
    Formula eight = all_eight_clauses();
    assert(!brute_sat(eight));
    assert(max_independent_set(reduce_to_independent_set(eight).graph).size() == 7);
    assert(max_independent_set(reduce_to_independent_set(eight, true, false).graph).size() == 8);
    assert(max_independent_set(reduce_to_independent_set(eight, false, true).graph).size() >= 8);
}

void test_coloring() {
    // Compuerta O: si las dos entradas son F, la salida es F; si alguna es T, la salida puede ser T.
    assert((or_gate_outputs(COLOR_F, COLOR_F) == std::array<bool, 3>{false, true, false}));
    for (int a : {COLOR_F, COLOR_T}) {
        for (int b : {COLOR_F, COLOR_T}) {
            if (a == COLOR_T || b == COLOR_T) assert(or_gate_outputs(a, b)[COLOR_T]);
        }
    }
    // Las 8 entradas del gadget.
    for (int mask = 0; mask < 8; mask++) {
        int count = clause_gadget_colorings(mask & 1, mask & 2, mask & 4);
        assert((count > 0) == (mask != 0));
    }
    // Tamaño y correspondencia con SAT.
    Random random(1403);
    for (int round = 0; round < 200; round++) {
        Formula f = random_three(random, 3 + below(random, 2), 1 + below(random, 10));
        Graph g = reduce_to_coloring(f);
        assert(g.size() == static_cast<std::size_t>(3 + 2 * f.variables) + 6 * f.clauses.size());
        assert(edge_count(g) == static_cast<std::size_t>(3 + 3 * f.variables) + 12 * f.clauses.size());
        auto sat = brute_sat(f);
        auto color = find_coloring(g, 3);
        assert(sat.has_value() == color.has_value());
        if (sat) assert(is_proper_coloring(g, coloring_from_assignment(f, *sat, g), 3));
        if (color) {
            // La lectura no depende del nombre de los colores.
            std::vector<int> names = {0, 1, 2};
            do {
                std::vector<int> renamed = *color;
                for (int& c : renamed) c = names[static_cast<std::size_t>(c)];
                assert(satisfies(f, assignment_from_coloring(f, renamed)));
            } while (std::next_permutation(names.begin(), names.end()));
        }
    }
    // Qué arista hace falta, en la fórmula sin solución.
    Formula eight = all_eight_clauses();
    assert(!find_coloring(reduce_to_coloring(eight), 3));
    GadgetOptions no_var;
    no_var.variable_to_b = false;
    assert(find_coloring(reduce_to_coloring(eight, no_var), 3));
    GadgetOptions no_f;
    no_f.output_to_f = false;
    assert(find_coloring(reduce_to_coloring(eight, no_f), 3));
    // La arista de la salida a B no es indispensable: con solo F la salida no puede ser F.
    GadgetOptions no_b;
    no_b.output_to_b = false;
    for (int round = 0; round < 60; round++) {
        Formula f = random_three(random, 3, 1 + below(random, 10));
        assert(brute_sat(f).has_value() == find_coloring(reduce_to_coloring(f, no_b), 3).has_value());
    }
    assert(!find_coloring(reduce_to_coloring(eight, no_b), 3));
}

void test_subset_sum() {
    Random random(1404);
    for (int round = 0; round < 400; round++) {
        int n = 1 + below(random, 6);
        Graph g = random_graph(random, n, 45);
        if (edge_count(g) > 9) continue;
        int cover = static_cast<int>(min_vertex_cover(g).size());
        for (int k = 0; k <= n + 2; k++) {
            SubsetSumInstance s = reduce_to_subset_sum(g, k);
            // Sin acarreos: en cada dígito de arista, todos los números juntos suman a lo sumo 3.
            for (std::size_t j = 0; j < s.edges.size(); j++) {
                Number digit_sum = 0;
                for (Number x : s.numbers) digit_sum += (x / power_of(4, j)) % 4;
                assert(digit_sum == 3);
            }
            auto chosen = brute_subset_sum(s.numbers, s.target);
            assert(chosen.has_value() == (cover <= k));
            // La base 3 también da bien: el ejercicio del capítulo pide demostrarlo.
            SubsetSumInstance three = reduce_to_subset_sum(g, k, 3);
            assert(brute_subset_sum(three.numbers, three.target).has_value() == (cover <= k));
            assert(subset_sum_dp(s.numbers, s.target) == (cover <= k));
            if (chosen) {
                std::vector<int> nodes = cover_from_subset(s, *chosen);
                assert(is_cover(g, nodes));
                assert(static_cast<int>(nodes.size()) == std::min(k, n));
            }
            if (cover <= k) {
                assert(sums_to_target(s, subset_from_cover(s, min_vertex_cover(g), k)));
            }
        }
    }
    // En base 2 hay una respuesta falsa: dos aristas separadas y k = 0.
    Graph two_edges = make_graph(4, {{0, 1}, {2, 3}});
    SubsetSumInstance base_two = reduce_to_subset_sum(two_edges, 0, 2);
    assert(brute_subset_sum(base_two.numbers, base_two.target).has_value());
    // Sin aristas, y con k = 0.
    Graph empty(3);
    assert(brute_subset_sum(reduce_to_subset_sum(empty, 0).numbers, reduce_to_subset_sum(empty, 0).target).has_value());
    // Con una arista y k = 0 no hay solución: la holgura sola da 1, y hacen falta 2.
    Graph edge = make_graph(2, {{0, 1}});
    assert(!brute_subset_sum(reduce_to_subset_sum(edge, 0).numbers, reduce_to_subset_sum(edge, 0).target));
}

void test_knapsack() {
    Random random(1405);
    for (int round = 0; round < 1500; round++) {
        std::vector<Item> items;
        int n = 1 + below(random, 7);
        for (int i = 0; i < n; i++) items.push_back({static_cast<Number>(1 + below(random, 12)), static_cast<Number>(below(random, 15))});
        Number capacity = static_cast<Number>(below(random, 30));
        int calls = 0;
        Number best = knapsack_optimum_by_search(items, capacity, calls);
        assert(best == knapsack_best(items, capacity));
        // Número de llamadas: a lo sumo ⌈log₂(suma + 1)⌉.
        Number total = 0;
        for (const Item& item : items) total += item.value;
        int bits = 0;
        while ((1ULL << bits) < total + 1) bits++;
        assert(calls <= bits);
        std::vector<std::size_t> chosen = knapsack_items_by_search(items, capacity);
        Number weight = 0;
        Number value = 0;
        for (std::size_t i : chosen) {
            weight += items[i].weight;
            value += items[i].value;
        }
        assert(weight <= capacity && value == best);
        // Suma de subconjuntos se reduce a la decisión de la mochila.
        std::vector<Number> numbers;
        for (int i = 0; i < n; i++) numbers.push_back(static_cast<Number>(1 + below(random, 20)));
        Number target = static_cast<Number>(below(random, 40));
        assert(knapsack_decide(knapsack_from_subset_sum(numbers, target)) == brute_subset_sum(numbers, target).has_value());
    }
}

void test_two_sat() {
    Random random(1406);
    int reversed_fails = 0;
    int unsatisfiable = 0;
    int half_wrong = 0;
    for (int round = 0; round < 6000; round++) {
        int n = 1 + below(random, 7);
        int m = below(random, 2 * n + 2);
        std::vector<TwoClause> clauses;
        for (int c = 0; c < m; c++) {
            int a = 1 + below(random, n);
            int b = 1 + below(random, n);
            // Incluye (x ∨ x) y (x ∨ ¬x), porque a y b pueden ser la misma variable.
            clauses.push_back({below(random, 2) ? a : -a, below(random, 2) ? b : -b});
        }
        Formula f = two_clauses_as_formula(n, clauses);
        auto brute = brute_sat(f);
        std::vector<int> comp = implication_components(implication_graph(n, clauses));
        // Una arista entre componentes va de la que salió más tarde a la que salió antes.
        ImplicationGraph g = implication_graph(n, clauses);
        for (std::size_t u = 0; u < g.size(); u++) {
            for (int v : g[u]) assert(comp[u] >= comp[static_cast<std::size_t>(v)]);
        }
        assert(same_component_clash(comp) != brute.has_value());
        auto solved = solve_two_sat(n, clauses);
        assert(solved.has_value() == brute.has_value());
        if (solved) {
            assert(satisfies(f, *solved));
            if (!satisfies(f, assignment_with_reversed_order(comp))) reversed_fails++;
        } else {
            unsatisfiable++;
        }
        if (same_component_clash(implication_components(implication_graph(n, clauses, false))) != !brute.has_value()) half_wrong++;
    }
    assert(reversed_fails > 0 && unsatisfiable > 0 && half_wrong > 0);
    // Con una sola arista por cláusula, la fórmula insatisfacible parece satisfacible.
    std::vector<TwoClause> hard = {{1, 2}, {1, -2}, {-1, 2}, {-1, -2}};
    assert(same_component_clash(implication_components(implication_graph(2, hard))));
    assert(!same_component_clash(implication_components(implication_graph(2, hard, false))));
    // (x1 ∨ x1) obliga a x1, y con el orden al revés sale falsa.
    std::vector<TwoClause> unit = {{1, 1}};
    assert(*solve_two_sat(1, unit) == Assignment({false, true}));
    assert(assignment_with_reversed_order(implication_components(implication_graph(1, unit))) == Assignment({false, false}));
}

void test_frontier() {
    Random random(1407);
    int odd_cycles = 0;
    for (int round = 0; round < 3000; round++) {
        int n = 1 + below(random, 7);
        Graph g = random_graph(random, n, 35);
        auto two = two_coloring(g);
        assert(two.has_value() == find_coloring(g, 2).has_value());
        if (two) assert(is_proper_coloring(g, *two, 2));
        else odd_cycles++;
        // Euler coincide con buscar el ciclo, y hace falta la conexión.
        if (edge_count(g) <= 10) assert(has_euler_cycle(g) == euler_cycle_brute(g));
    }
    assert(odd_cycles > 0);
    Graph two_triangles = make_graph(6, {{0, 1}, {1, 2}, {0, 2}, {3, 4}, {4, 5}, {3, 5}});
    for (const auto& list : two_triangles) assert(list.size() % 2 == 0);
    assert(!has_euler_cycle(two_triangles));
    // Camino más largo en un DAG: los nodos están numerados en orden topológico.
    for (int round = 0; round < 3000; round++) {
        int n = 1 + below(random, 8);
        Dag dag(static_cast<std::size_t>(n));
        for (int u = 0; u < n; u++) {
            for (int v = u + 1; v < n; v++) {
                if (below(random, 100) < 40) dag[static_cast<std::size_t>(u)].push_back(v);
            }
        }
        assert(longest_path_dag(dag) == longest_path_dag_brute(dag));
    }
    Graph square = make_graph(4, {{0, 1}, {1, 2}, {2, 3}, {0, 3}});
    Graph star = make_graph(4, {{0, 1}, {0, 2}, {0, 3}});
    assert(longest_simple_path(square) == 3);
    assert(longest_simple_path(star) == 2);
}

void test_complement() {
    // Lo que se usa de la semana 13: S es independiente si y solo si V − S es una cobertura.
    Random random(1408);
    for (int round = 0; round < 500; round++) {
        int n = 1 + below(random, 8);
        Graph g = random_graph(random, n, 40);
        assert(max_independent_set(g).size() + min_vertex_cover(g).size() == static_cast<std::size_t>(n));
    }
}

}  // namespace

int main() {
    test_three_sat();
    test_independent_set();
    test_coloring();
    test_subset_sum();
    test_knapsack();
    test_two_sat();
    test_frontier();
    test_complement();
    std::cout << "Todas las pruebas de la semana 14 pasaron.\n";
}