// Fórmulas en CNF. Un literal es un entero: +v es la variable v, y -v es su negación. Las variables
// se numeran desde 1, como en DIMACS.
#pragma once
#include <cstddef>
#include <cstdlib>
#include <optional>
#include <string>
#include <vector>

using Clause = std::vector<int>;

struct Formula {
    int variables = 0;
    std::vector<Clause> clauses;
};

// Assignment[v] es el valor de la variable v. La posición 0 no se usa.
using Assignment = std::vector<bool>;

inline bool literal_true(const Assignment& a, int literal) {
    bool value = a[static_cast<std::size_t>(std::abs(literal))];
    return literal > 0 ? value : !value;
}

inline bool clause_true(const Assignment& a, const Clause& c) {
    for (int literal : c) {
        if (literal_true(a, literal)) return true;
    }
    return false;
}

// El verificador de SAT: el certificado es la asignación, y revisarla es lineal en la fórmula.
inline bool satisfies(const Formula& f, const Assignment& a) {
    for (const Clause& c : f.clauses) {
        if (!clause_true(a, c)) return false;
    }
    return true;
}

// Fuerza bruta: prueba las 2ⁿ asignaciones. Solo para fórmulas pequeñas.
inline std::optional<Assignment> brute_sat(const Formula& f) {
    const std::size_t n = static_cast<std::size_t>(f.variables);
    for (unsigned long long mask = 0; mask < (1ULL << n); mask++) {
        Assignment a(n + 1, false);
        for (std::size_t v = 1; v <= n; v++) a[v] = (mask >> (v - 1)) & 1;
        if (satisfies(f, a)) return a;
    }
    return std::nullopt;
}

inline std::string literal_text(int literal) {
    return (literal < 0 ? "¬x" : "x") + std::to_string(std::abs(literal));
}

inline std::string clause_text(const Clause& c) {
    std::string text = "(";
    for (std::size_t i = 0; i < c.size(); i++) text += (i ? " ∨ " : "") + literal_text(c[i]);
    return text + ")";
}

inline std::string formula_text(const Formula& f) {
    std::string text;
    for (std::size_t i = 0; i < f.clauses.size(); i++) text += (i ? " ∧ " : "") + clause_text(f.clauses[i]);
    return text;
}

inline std::string assignment_text(const Assignment& a) {
    std::string text;
    for (std::size_t v = 1; v < a.size(); v++) {
        text += (v > 1 ? " " : "") + ("x" + std::to_string(v)) + "=" + (a[v] ? "V" : "F");
    }
    return text;
}

// Las ocho cláusulas posibles con tres variables: ninguna asignación las cumple todas.
inline Formula all_eight_clauses() {
    Formula f{3, {}};
    for (int mask = 0; mask < 8; mask++) {
        f.clauses.push_back({mask & 1 ? 1 : -1, mask & 2 ? 2 : -2, mask & 4 ? 3 : -3});
    }
    return f;
}

// La reducción de 3-SAT a 3-coloreo: la compuerta O, las 8 entradas de la cláusula y una fórmula completa.
#include <iostream>
#include <string>
#include "coloring.h"

namespace {

char color_name(int c) { return "TFB"[c]; }

std::string outputs_text(const std::array<bool, 3>& possible) {
    std::string text;
    for (int c = 0; c < 3; c++) {
        if (possible[static_cast<std::size_t>(c)]) text += std::string(text.empty() ? "" : " ") + color_name(c);
    }
    return text.empty() ? "ninguno" : text;
}

void solve(const Formula& f) {
    Graph g = reduce_to_coloring(f);
    std::cout << formula_text(f) << '\n';
    std::cout << "  " << g.size() << " nodos, " << edge_count(g) << " aristas\n";
    auto color = find_coloring(g, 3);
    auto sat = brute_sat(f);
    std::cout << "  ¿3-coloreable? " << (color ? "sí" : "no") << ", fuerza bruta sobre la fórmula: "
              << (sat ? "satisfacible" : "insatisfacible") << '\n';
    if (color) {
        Assignment a = assignment_from_coloring(f, *color);
        std::cout << "  lectura del coloreo: " << assignment_text(a) << ", ¿cumple? " << (satisfies(f, a) ? "sí" : "no") << '\n';
    }
}

}  // namespace

int main() {
    std::cout << "Una compuerta O: qué colores admite la salida r.\n";
    std::cout << "  a b | r\n";
    for (int a : {COLOR_F, COLOR_T}) {
        for (int b : {COLOR_F, COLOR_T}) {
            std::cout << "  " << color_name(a) << ' ' << color_name(b) << " | " << outputs_text(or_gate_outputs(a, b)) << '\n';
        }
    }
    std::cout << "\nLa segunda compuerta puede recibir B, porque r no está unido a B.\n";
    std::cout << "  a b | r\n";
    for (int b : {COLOR_F, COLOR_T}) {
        std::cout << "  B " << color_name(b) << " | " << outputs_text(or_gate_outputs(COLOR_B, b)) << '\n';
    }

    std::cout << "\nEl gadget de cláusula: coloreos de sus 6 nodos internos, de 3^6 = 729 posibles.\n";
    std::cout << "  a b c | coloreos\n";
    for (int mask = 0; mask < 8; mask++) {
        bool a = mask & 4;
        bool b = mask & 2;
        bool c = mask & 1;
        std::cout << "  " << (a ? 'T' : 'F') << ' ' << (b ? 'T' : 'F') << ' ' << (c ? 'T' : 'F') << " | "
                  << clause_gadget_colorings(a, b, c) << '\n';
    }

    std::cout << "\nFórmulas completas:\n";
    solve({3, {{1, -2, 3}, {-1, 2, -3}}});
    solve({3, {{1, 2, 3}, {-1, -2, 3}, {1, -2, -3}}});
    solve(all_eight_clauses());

    std::cout << "\nSi faltan aristas, en la fórmula de ocho cláusulas, que no tiene solución:\n";
    Formula eight = all_eight_clauses();
    GadgetOptions no_var;
    no_var.variable_to_b = false;
    std::cout << "  variables sin arista a B:      "
              << (find_coloring(reduce_to_coloring(eight, no_var), 3) ? "3-coloreable" : "no 3-coloreable") << '\n';
    GadgetOptions no_f;
    no_f.output_to_f = false;
    std::cout << "  salida sin arista a F:         "
              << (find_coloring(reduce_to_coloring(eight, no_f), 3) ? "3-coloreable" : "no 3-coloreable") << '\n';
    GadgetOptions no_b;
    no_b.output_to_b = false;
    std::cout << "  salida sin arista a B:         "
              << (find_coloring(reduce_to_coloring(eight, no_b), 3) ? "3-coloreable" : "no 3-coloreable") << '\n';
}

// La reducción de 3-SAT a 3-coloreo. La paleta es un triángulo T, F, B. Cada variable es un par de nodos
// unidos entre sí y con B. Cada cláusula es una cadena de dos compuertas O, cuya salida se une a F y a B.
#pragma once
#include <array>
#include <cstddef>
#include <cstdlib>
#include <vector>
#include "cnf.h"
#include "graph.h"

constexpr int COLOR_T = 0;
constexpr int COLOR_F = 1;
constexpr int COLOR_B = 2;

// Los tres primeros nodos del grafo son la paleta, y luego vienen x1, ¬x1, x2, ¬x2, ...
constexpr int NODE_T = 0;
constexpr int NODE_F = 1;
constexpr int NODE_B = 2;

inline int literal_node(int literal) {
    int v = std::abs(literal);
    return 3 + 2 * (v - 1) + (literal > 0 ? 0 : 1);
}

// Qué aristas poner, para ver qué se rompe si falta alguna.
struct GadgetOptions {
    bool variable_to_b = true;
    bool output_to_f = true;
    bool output_to_b = true;
};

// Compuerta O: agrega los nodos p, q, r con a-p, b-q, p-q, p-r, q-r. Devuelve r, la salida.
inline int add_or_gate(Graph& g, int a, int b) {
    int p = static_cast<int>(g.size());
    int q = p + 1;
    int r = p + 2;
    g.resize(g.size() + 3);
    add_edge(g, a, p);
    add_edge(g, b, q);
    add_edge(g, p, q);
    add_edge(g, p, r);
    add_edge(g, q, r);
    return r;
}

// Cláusula de tres literales: la salida de la segunda compuerta queda obligada a ser T.
inline void add_clause_gadget(Graph& g, int a, int b, int c, const GadgetOptions& options = {}) {
    int first = add_or_gate(g, a, b);
    int output = add_or_gate(g, first, c);
    if (options.output_to_f) add_edge(g, output, NODE_F);
    if (options.output_to_b) add_edge(g, output, NODE_B);
}

inline Graph reduce_to_coloring(const Formula& f, const GadgetOptions& options = {}) {
    Graph g(static_cast<std::size_t>(3 + 2 * f.variables));
    add_edge(g, NODE_T, NODE_F);
    add_edge(g, NODE_F, NODE_B);
    add_edge(g, NODE_T, NODE_B);
    for (int v = 1; v <= f.variables; v++) {
        add_edge(g, literal_node(v), literal_node(-v));
        if (options.variable_to_b) {
            add_edge(g, literal_node(v), NODE_B);
            add_edge(g, literal_node(-v), NODE_B);
        }
    }
    for (const Clause& c : f.clauses) {
        add_clause_gadget(g, literal_node(c[0]), literal_node(c[1]), literal_node(c[2]), options);
    }
    return g;
}

// De un coloreo a una asignación. Los colores no traen nombre: T es el color que recibió el nodo T.
inline Assignment assignment_from_coloring(const Formula& f, const std::vector<int>& color) {
    Assignment a(static_cast<std::size_t>(f.variables) + 1, false);
    for (int v = 1; v <= f.variables; v++) {
        a[static_cast<std::size_t>(v)] = color[static_cast<std::size_t>(literal_node(v))] == color[NODE_T];
    }
    return a;
}

// Colorea una compuerta dados los colores de sus entradas: T en la salida si alguna entrada es T, y si
// no, F. Es la construcción de la demostración.
inline int color_or_gate(std::vector<int>& color, std::size_t p, int a_color, int b_color) {
    int q_color = COLOR_B;
    int p_color = COLOR_B;
    int r_color = COLOR_F;
    if (a_color == COLOR_T) {
        r_color = COLOR_T;
        p_color = b_color == COLOR_T ? COLOR_B : COLOR_F;
        q_color = b_color == COLOR_T ? COLOR_F : COLOR_B;
    } else if (b_color == COLOR_T) {
        r_color = COLOR_T;
        p_color = COLOR_B;
        q_color = COLOR_F;
    } else {
        p_color = COLOR_T;
        q_color = COLOR_B;
    }
    color[p] = p_color;
    color[p + 1] = q_color;
    color[p + 2] = r_color;
    return r_color;
}

// De una asignación que cumple la fórmula a un coloreo, sin buscar.
inline std::vector<int> coloring_from_assignment(const Formula& f, const Assignment& a, const Graph& g) {
    std::vector<int> color(g.size(), -1);
    color[NODE_T] = COLOR_T;
    color[NODE_F] = COLOR_F;
    color[NODE_B] = COLOR_B;
    for (int v = 1; v <= f.variables; v++) {
        bool value = a[static_cast<std::size_t>(v)];
        color[static_cast<std::size_t>(literal_node(v))] = value ? COLOR_T : COLOR_F;
        color[static_cast<std::size_t>(literal_node(-v))] = value ? COLOR_F : COLOR_T;
    }
    std::size_t next = static_cast<std::size_t>(3 + 2 * f.variables);
    for (const Clause& c : f.clauses) {
        int first = color_or_gate(color, next, literal_true(a, c[0]) ? COLOR_T : COLOR_F, literal_true(a, c[1]) ? COLOR_T : COLOR_F);
        color_or_gate(color, next + 3, first, literal_true(a, c[2]) ? COLOR_T : COLOR_F);
        next += 6;
    }
    return color;
}

// Una compuerta sola con la paleta y sus entradas ya coloreadas: qué colores admite la salida.
// Devuelve, para cada color posible de r, si existe un coloreo de p y q que lo permita.
inline std::array<bool, 3> or_gate_outputs(int a_color, int b_color) {
    std::array<bool, 3> possible = {false, false, false};
    for (int p = 0; p < 3; p++) {
        for (int q = 0; q < 3; q++) {
            for (int r = 0; r < 3; r++) {
                if (p != a_color && q != b_color && p != q && p != r && q != r) possible[static_cast<std::size_t>(r)] = true;
            }
        }
    }
    return possible;
}

// Enumera los coloreos de los 6 nodos internos del gadget de cláusula, con T, F, B y las tres entradas
// fijas. Cuenta cuántos son propios. Son 3⁶ posibilidades para cada una de las 8 entradas.
inline int clause_gadget_colorings(bool a, bool b, bool c) {
    Graph g(6);
    add_edge(g, NODE_T, NODE_F);
    add_edge(g, NODE_F, NODE_B);
    add_edge(g, NODE_T, NODE_B);
    add_edge(g, 3, NODE_B);
    add_edge(g, 4, NODE_B);
    add_edge(g, 5, NODE_B);
    add_clause_gadget(g, 3, 4, 5);
    std::vector<int> color(g.size(), 0);
    color[NODE_T] = COLOR_T;
    color[NODE_F] = COLOR_F;
    color[NODE_B] = COLOR_B;
    color[3] = a ? COLOR_T : COLOR_F;
    color[4] = b ? COLOR_T : COLOR_F;
    color[5] = c ? COLOR_T : COLOR_F;
    int total = 0;
    for (int mask = 0; mask < 729; mask++) {
        int rest = mask;
        for (std::size_t v = 6; v < 12; v++) {
            color[v] = rest % 3;
            rest /= 3;
        }
        if (is_proper_coloring(g, color, 3)) total++;
    }
    return total;
}

// Pregunta de repaso 4, con un ejemplo de cada problema y la fuerza bruta al lado.
#include <iostream>
#include "frontier.h"
#include "two_sat.h"

int main() {
    Dag dag = {{1, 2}, {3}, {3, 4}, {5}, {5}, {}};
    std::cout << "Camino más largo en un DAG de 6 nodos: " << longest_path_dag(dag) << " aristas, fuerza bruta "
              << longest_path_dag_brute(dag) << '\n';

    Graph triangle = make_graph(3, {{0, 1}, {1, 2}, {0, 2}});
    Graph square = make_graph(4, {{0, 1}, {1, 2}, {2, 3}, {0, 3}});
    std::cout << "2-coloreo: triángulo " << (two_coloring(triangle) ? "sí" : "no") << " (3 colores: "
              << (find_coloring(triangle, 3) ? "sí" : "no") << "), cuadrado " << (two_coloring(square) ? "sí" : "no") << '\n';

    Graph bowtie = make_graph(5, {{0, 1}, {1, 2}, {0, 2}, {2, 3}, {3, 4}, {2, 4}});
    Graph two_triangles = make_graph(6, {{0, 1}, {1, 2}, {0, 2}, {3, 4}, {4, 5}, {3, 5}});
    Graph tail = make_graph(4, {{0, 1}, {1, 2}, {0, 2}, {2, 3}});
    auto euler_line = [](const char* name, const Graph& g) {
        std::cout << "  " << name << ": grados y conexión " << (has_euler_cycle(g) ? "sí" : "no") << ", fuerza bruta "
                  << (euler_cycle_brute(g) ? "sí" : "no") << '\n';
    };
    std::cout << "¿Ciclo que use cada arista exactamente una vez?\n";
    euler_line("dos triángulos con un nodo común", bowtie);
    euler_line("dos triángulos separados        ", two_triangles);
    euler_line("triángulo con una cola          ", tail);

    std::cout << "Camino simple más largo, y camino hamiltoniano:\n";
    Graph star = make_graph(4, {{0, 1}, {0, 2}, {0, 3}});
    std::cout << "  cuadrado: " << longest_simple_path(square) << " aristas, de V − 1 = 3: hamiltoniano\n";
    std::cout << "  estrella: " << longest_simple_path(star) << " aristas, de V − 1 = 3: no hamiltoniano\n";

    std::vector<TwoClause> clauses = {{1, 2}, {-1, 3}, {-2, -3}};
    auto a = solve_two_sat(3, clauses);
    std::cout << "2-SAT: " << formula_text(two_clauses_as_formula(3, clauses)) << ": " << (a ? assignment_text(*a) : "insatisfacible") << '\n';
}

// Los problemas fáciles que están al lado de los difíciles, y fuerzas brutas para comprobarlos.
#pragma once
#include <algorithm>
#include <cstddef>
#include <numeric>
#include <optional>
#include <queue>
#include <utility>
#include <vector>
#include "graph.h"

// 2-coloreo con BFS: cada nodo recibe el color contrario al de quien lo descubrió, y una arista entre
// dos nodos del mismo color es un ciclo impar.
inline std::optional<std::vector<int>> two_coloring(const Graph& g) {
    std::vector<int> color(g.size(), -1);
    std::queue<int> pending;
    for (std::size_t s = 0; s < g.size(); s++) {
        if (color[s] != -1) continue;
        color[s] = 0;
        pending.push(static_cast<int>(s));
        while (!pending.empty()) {
            std::size_t u = static_cast<std::size_t>(pending.front());
            pending.pop();
            for (int w : g[u]) {
                std::size_t v = static_cast<std::size_t>(w);
                if (color[v] == -1) {
                    color[v] = 1 - color[u];
                    pending.push(w);
                } else if (color[v] == color[u]) {
                    return std::nullopt;
                }
            }
        }
    }
    return color;
}

// Euler: todo grado par, y todas las aristas en una sola componente. Los nodos aislados no estorban.
inline bool has_euler_cycle(const Graph& g) {
    std::vector<char> seen(g.size(), 0);
    std::size_t start = g.size();
    for (std::size_t v = 0; v < g.size(); v++) {
        if (g[v].size() % 2 != 0) return false;
        if (start == g.size() && !g[v].empty()) start = v;
    }
    if (start == g.size()) return true;
    std::vector<std::size_t> stack = {start};
    seen[start] = 1;
    while (!stack.empty()) {
        std::size_t u = stack.back();
        stack.pop_back();
        for (int w : g[u]) {
            if (!seen[static_cast<std::size_t>(w)]) {
                seen[static_cast<std::size_t>(w)] = 1;
                stack.push_back(static_cast<std::size_t>(w));
            }
        }
    }
    for (std::size_t v = 0; v < g.size(); v++) {
        if (!g[v].empty() && !seen[v]) return false;
    }
    return true;
}

// Fuerza bruta: busca un ciclo que use cada arista exactamente una vez, probando continuaciones.
inline bool euler_search(const std::vector<std::pair<int, int>>& edges, std::vector<char>& used, int at, int start, std::size_t count) {
    if (count == edges.size()) return at == start;
    for (std::size_t e = 0; e < edges.size(); e++) {
        if (used[e]) continue;
        auto [u, v] = edges[e];
        if (u != at && v != at) continue;
        used[e] = 1;
        if (euler_search(edges, used, u == at ? v : u, start, count + 1)) {
            used[e] = 0;
            return true;
        }
        used[e] = 0;
    }
    return false;
}

inline bool euler_cycle_brute(const Graph& g) {
    std::vector<std::pair<int, int>> edges = edge_list(g);
    if (edges.empty()) return true;
    std::vector<char> used(edges.size(), 0);
    return euler_search(edges, used, edges[0].first, edges[0].first, 0);
}

// Hay camino hamiltoniano si el camino simple más largo tiene V − 1 aristas. Fuerza bruta, grafo no dirigido.
inline int longest_from(const Graph& g, std::size_t u, std::vector<char>& used) {
    int best = 0;
    used[u] = 1;
    for (int w : g[u]) {
        if (!used[static_cast<std::size_t>(w)]) best = std::max(best, 1 + longest_from(g, static_cast<std::size_t>(w), used));
    }
    used[u] = 0;
    return best;
}

inline int longest_simple_path(const Graph& g) {
    int best = 0;
    std::vector<char> used(g.size(), 0);
    for (std::size_t s = 0; s < g.size(); s++) best = std::max(best, longest_from(g, s, used));
    return best;
}

// Grafos dirigidos para el camino más largo en un DAG, medido en aristas.
using Dag = std::vector<std::vector<int>>;

// L[u] es el mayor número de aristas de un camino que sale de u. Los sucesores se calculan primero.
inline int longest_path_dag(const Dag& g) {
    std::vector<int> pending(g.size(), 0);
    Dag inverse(g.size());
    for (std::size_t u = 0; u < g.size(); u++) {
        pending[u] = static_cast<int>(g[u].size());
        for (int v : g[u]) inverse[static_cast<std::size_t>(v)].push_back(static_cast<int>(u));
    }
    std::vector<int> ready;
    for (std::size_t u = 0; u < g.size(); u++) {
        if (pending[u] == 0) ready.push_back(static_cast<int>(u));
    }
    std::vector<int> length(g.size(), 0);
    int best = 0;
    while (!ready.empty()) {
        std::size_t u = static_cast<std::size_t>(ready.back());
        ready.pop_back();
        best = std::max(best, length[u]);
        for (int w : inverse[u]) {
            std::size_t p = static_cast<std::size_t>(w);
            length[p] = std::max(length[p], length[u] + 1);
            if (--pending[p] == 0) ready.push_back(w);
        }
    }
    return best;
}

inline int longest_directed_from(const Dag& g, std::size_t u) {
    int best = 0;
    for (int v : g[u]) best = std::max(best, 1 + longest_directed_from(g, static_cast<std::size_t>(v)));
    return best;
}

inline int longest_path_dag_brute(const Dag& g) {
    int best = 0;
    for (std::size_t u = 0; u < g.size(); u++) best = std::max(best, longest_directed_from(g, u));
    return best;
}

// Grafos no dirigidos simples y las fuerzas brutas que sirven de referencia en esta semana.
#pragma once
#include <algorithm>
#include <cstddef>
#include <optional>
#include <utility>
#include <vector>

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

inline void add_edge(Graph& g, int u, int v) {
    g[static_cast<std::size_t>(u)].push_back(v);
    g[static_cast<std::size_t>(v)].push_back(u);
}

inline Graph make_graph(int n, const std::vector<std::pair<int, int>>& edges) {
    Graph g(static_cast<std::size_t>(n));
    for (auto [u, v] : edges) add_edge(g, u, v);
    return g;
}

inline std::vector<std::pair<int, int>> edge_list(const Graph& g) {
    std::vector<std::pair<int, int>> edges;
    for (std::size_t u = 0; u < g.size(); u++) {
        for (int v : g[u]) {
            if (static_cast<int>(u) < v) edges.push_back({static_cast<int>(u), v});
        }
    }
    return edges;
}

inline std::size_t edge_count(const Graph& g) {
    std::size_t total = 0;
    for (const auto& list : g) total += list.size();
    return total / 2;
}

// Verificadores: el certificado es el conjunto, y se revisa en tiempo polinomial.
inline bool is_independent(const Graph& g, const std::vector<int>& nodes) {
    std::vector<char> inside(g.size(), 0);
    for (int v : nodes) {
        if (inside[static_cast<std::size_t>(v)]) return false;
        inside[static_cast<std::size_t>(v)] = 1;
    }
    for (int v : nodes) {
        for (int w : g[static_cast<std::size_t>(v)]) {
            if (inside[static_cast<std::size_t>(w)]) return false;
        }
    }
    return true;
}

inline bool is_cover(const Graph& g, const std::vector<int>& nodes) {
    std::vector<char> inside(g.size(), 0);
    for (int v : nodes) inside[static_cast<std::size_t>(v)] = 1;
    for (auto [u, v] : edge_list(g)) {
        if (!inside[static_cast<std::size_t>(u)] && !inside[static_cast<std::size_t>(v)]) return false;
    }
    return true;
}

inline bool is_proper_coloring(const Graph& g, const std::vector<int>& color, int colors) {
    for (std::size_t u = 0; u < g.size(); u++) {
        if (color[u] < 0 || color[u] >= colors) return false;
        for (int v : g[u]) {
            if (color[u] == color[static_cast<std::size_t>(v)]) return false;
        }
    }
    return true;
}

// Conjunto independiente máximo: en cada nodo, tomarlo o no. Exponencial; solo para grafos pequeños.
inline void independent_search(const Graph& g, std::size_t v, std::vector<int>& blocked, std::vector<int>& current,
                               std::vector<int>& best) {
    if (current.size() + (g.size() - v) <= best.size()) return;
    if (v == g.size()) {
        best = current;
        return;
    }
    if (blocked[v] == 0) {
        for (int w : g[v]) blocked[static_cast<std::size_t>(w)]++;
        current.push_back(static_cast<int>(v));
        independent_search(g, v + 1, blocked, current, best);
        current.pop_back();
        for (int w : g[v]) blocked[static_cast<std::size_t>(w)]--;
    }
    independent_search(g, v + 1, blocked, current, best);
}

inline std::vector<int> max_independent_set(const Graph& g) {
    std::vector<int> blocked(g.size(), 0);
    std::vector<int> current;
    std::vector<int> best;
    independent_search(g, 0, blocked, current, best);
    return best;
}

// Cobertura mínima, probando los 2^V subconjuntos.
inline std::vector<int> min_vertex_cover(const Graph& g) {
    const std::size_t n = g.size();
    std::vector<int> best;
    for (std::size_t i = 0; i < n; i++) best.push_back(static_cast<int>(i));
    for (unsigned long long mask = 0; mask < (1ULL << n); mask++) {
        std::vector<int> nodes;
        for (std::size_t i = 0; i < n; i++) {
            if ((mask >> i) & 1) nodes.push_back(static_cast<int>(i));
        }
        if (nodes.size() < best.size() && is_cover(g, nodes)) best = nodes;
    }
    return best;
}

// Backtracking para colorear con k colores, nodo por nodo.
inline bool color_search(const Graph& g, std::size_t v, int k, std::vector<int>& color) {
    if (v == g.size()) return true;
    for (int c = 0; c < k; c++) {
        bool free = true;
        for (int w : g[v]) {
            if (color[static_cast<std::size_t>(w)] == c) free = false;
        }
        if (!free) continue;
        color[v] = c;
        if (color_search(g, v + 1, k, color)) return true;
        color[v] = -1;
    }
    return false;
}

inline std::optional<std::vector<int>> find_coloring(const Graph& g, int k) {
    std::vector<int> color(g.size(), -1);
    if (color_search(g, 0, k, color)) return color;
    return std::nullopt;
}

// La reducción de 3-SAT a conjunto independiente: un triángulo por cláusula y una arista entre cada
// par de literales opuestos. La fórmula se cumple si y solo si hay un conjunto independiente de tamaño k,
// con k igual al número de cláusulas.
#pragma once
#include <cstddef>
#include <vector>
#include "cnf.h"
#include "graph.h"

struct IndependentSetInstance {
    Graph graph;
    int k = 0;
    std::vector<int> literal;  // literal[nodo] es el literal que representa ese nodo
};

// Las dos banderas existen para ver qué pasa si falta cada clase de aristas.
inline IndependentSetInstance reduce_to_independent_set(const Formula& f, bool triangles = true, bool conflicts = true) {
    IndependentSetInstance out;
    out.k = static_cast<int>(f.clauses.size());
    for (const Clause& c : f.clauses) out.literal.insert(out.literal.end(), c.begin(), c.end());
    out.graph.assign(out.literal.size(), {});
    int base = 0;
    for (const Clause& c : f.clauses) {
        int size = static_cast<int>(c.size());
        for (int i = 0; triangles && i < size; i++) {
            for (int j = i + 1; j < size; j++) add_edge(out.graph, base + i, base + j);
        }
        base += size;
    }
    int nodes = static_cast<int>(out.literal.size());
    for (int u = 0; conflicts && u < nodes; u++) {
        for (int v = u + 1; v < nodes; v++) {
            if (out.literal[static_cast<std::size_t>(u)] == -out.literal[static_cast<std::size_t>(v)]) add_edge(out.graph, u, v);
        }
    }
    return out;
}

// De una asignación a un conjunto: el primer literal verdadero de cada cláusula.
inline std::vector<int> set_from_assignment(const Formula& f, const Assignment& a) {
    std::vector<int> nodes;
    int base = 0;
    for (const Clause& c : f.clauses) {
        for (std::size_t i = 0; i < c.size(); i++) {
            if (literal_true(a, c[i])) {
                nodes.push_back(base + static_cast<int>(i));
                break;
            }
        }
        base += static_cast<int>(c.size());
    }
    return nodes;
}

// De un conjunto a una asignación: lo elegido es verdadero. El resto de variables da igual: quedan en F.
inline Assignment assignment_from_set(const Formula& f, const IndependentSetInstance& instance, const std::vector<int>& nodes) {
    Assignment a(static_cast<std::size_t>(f.variables) + 1, false);
    for (int v : nodes) {
        int literal = instance.literal[static_cast<std::size_t>(v)];
        a[static_cast<std::size_t>(std::abs(literal))] = literal > 0;
    }
    return a;
}

// La reducción de 3-SAT a conjunto independiente: el grafo, la respuesta y lo que pasa si faltan aristas.
#include <iostream>
#include <string>
#include "independent_set.h"

namespace {

std::string node_name(const IndependentSetInstance& s, int v) {
    return std::to_string(v) + ":" + literal_text(s.literal[static_cast<std::size_t>(v)]);
}

void show_graph(const IndependentSetInstance& s) {
    std::cout << "  nodos:";
    for (int v = 0; v < static_cast<int>(s.literal.size()); v++) std::cout << ' ' << node_name(s, v);
    std::cout << "\n  aristas de literales opuestos:";
    for (auto [u, v] : edge_list(s.graph)) {
        if (s.literal[static_cast<std::size_t>(u)] == -s.literal[static_cast<std::size_t>(v)]) std::cout << ' ' << u << '-' << v;
    }
    std::cout << '\n';
}

void solve(const Formula& f) {
    IndependentSetInstance s = reduce_to_independent_set(f);
    std::cout << formula_text(f) << '\n';
    show_graph(s);
    std::vector<int> best = max_independent_set(s.graph);
    std::cout << "  k = " << s.k << ", conjunto independiente máximo: " << best.size() << " (";
    for (std::size_t i = 0; i < best.size(); i++) std::cout << (i ? ", " : "") << node_name(s, best[i]);
    std::cout << ")\n";
    auto sat = brute_sat(f);
    std::cout << "  fuerza bruta sobre la fórmula: " << (sat ? "satisfacible, " + assignment_text(*sat) : "insatisfacible") << '\n';
    if (static_cast<int>(best.size()) >= s.k) {
        Assignment a = assignment_from_set(f, s, best);
        std::cout << "  lectura del conjunto: " << assignment_text(a) << ", ¿cumple? " << (satisfies(f, a) ? "sí" : "no") << '\n';
    }
    std::cout << '\n';
}

}  // namespace

int main() {
    std::cout << "Dos cláusulas (pregunta de repaso 2):\n";
    solve({3, {{1, -2, 3}, {-1, 2, -3}}});

    std::cout << "El ejemplo del texto:\n";
    solve({3, {{1, 2, 3}, {-1, -2, 3}, {1, -2, -3}}});

    std::cout << "Sin solución: las ocho cláusulas sobre tres variables.\n";
    Formula eight = all_eight_clauses();
    IndependentSetInstance s = reduce_to_independent_set(eight);
    std::cout << "  " << s.literal.size() << " nodos, " << edge_count(s.graph) << " aristas, k = " << s.k
              << ", máximo: " << max_independent_set(s.graph).size() << "\n\n";

    std::cout << "Si faltan aristas, en esa misma fórmula insatisfacible:\n";
    IndependentSetInstance no_conflicts = reduce_to_independent_set(eight, true, false);
    std::cout << "  sin literales opuestos: máximo " << max_independent_set(no_conflicts.graph).size() << ", k = " << s.k << '\n';
    IndependentSetInstance no_triangles = reduce_to_independent_set(eight, false, true);
    std::cout << "  sin triángulos:         máximo " << max_independent_set(no_triangles.graph).size() << ", k = " << s.k << '\n';
}

// De la decisión a la optimización, usando la decisión como una caja negra.
#include <iostream>
#include "knapsack_search.h"

int main() {
    std::vector<Item> items = {{4, 10}, {3, 7}, {2, 4}, {5, 12}, {1, 1}};
    const Number capacity = 9;
    int calls = 0;
    Number total = 0;
    for (const Item& item : items) total += item.value;
    Number best = knapsack_optimum_by_search(items, capacity, calls);
    std::cout << "objetos (peso, valor):";
    for (const Item& item : items) std::cout << " (" << item.weight << ", " << item.value << ")";
    std::cout << "\ncapacidad " << capacity << ", suma de valores " << total << '\n';
    std::cout << "óptimo por búsqueda binaria: " << best << ", con " << calls << " llamadas a la decisión\n";
    std::cout << "óptimo por la tabla de la semana 7: " << knapsack_best(items, capacity) << '\n';
    std::cout << "objetos elegidos, con otra llamada por objeto:";
    for (std::size_t i : knapsack_items_by_search(items, capacity)) std::cout << ' ' << i;
    std::cout << '\n';
    std::vector<Number> numbers = {3, 5, 9};
    for (Number target : {8ULL, 10ULL}) {
        KnapsackDecision d = knapsack_from_subset_sum(numbers, target);
        std::cout << "suma de subconjuntos {3, 5, 9} con objetivo " << target << ": mochila dice "
                  << (knapsack_decide(d) ? "sí" : "no") << ", fuerza bruta dice "
                  << (brute_subset_sum(numbers, target) ? "sí" : "no") << '\n';
    }
}

// La mochila en su versión de decisión: ¿hay objetos con peso a lo sumo W y valor al menos V? Suma de
// subconjuntos se reduce a ella, y con una caja negra para la decisión se recupera la de optimización.
#pragma once
#include <cstddef>
#include <vector>
#include "subset_sum.h"

struct Item {
    Number weight;
    Number value;
};

struct KnapsackDecision {
    std::vector<Item> items;
    Number capacity;
    Number goal;
};

// Peso y valor iguales al número, y capacidad y meta iguales al objetivo.
inline KnapsackDecision knapsack_from_subset_sum(const std::vector<Number>& numbers, Number target) {
    KnapsackDecision out{{}, target, target};
    for (Number x : numbers) out.items.push_back({x, x});
    return out;
}

// La mejor ganancia con capacidad W, en O(nW), como en la semana 7.
inline Number knapsack_best(const std::vector<Item>& items, Number capacity) {
    std::vector<Number> best(static_cast<std::size_t>(capacity) + 1, 0);
    for (const Item& item : items) {
        for (std::size_t c = static_cast<std::size_t>(capacity) + 1; c-- > static_cast<std::size_t>(item.weight);) {
            best[c] = std::max(best[c], best[c - static_cast<std::size_t>(item.weight)] + item.value);
        }
    }
    return best[static_cast<std::size_t>(capacity)];
}

inline bool knapsack_decide(const KnapsackDecision& d) {
    return knapsack_best(d.items, d.capacity) >= d.goal;
}

// Búsqueda binaria sobre el valor, llamando solo a la decisión. Cuenta las llamadas.
inline Number knapsack_optimum_by_search(const std::vector<Item>& items, Number capacity, int& calls) {
    Number low = 0;
    Number high = 0;
    for (const Item& item : items) high += item.value;
    calls = 0;
    // Invariante: se puede alcanzar low, y no se puede alcanzar nada mayor que high.
    while (low < high) {
        Number middle = low + (high - low + 1) / 2;
        calls++;
        if (knapsack_decide({items, capacity, middle})) low = middle;
        else high = middle - 1;
    }
    return low;
}

// Qué objetos llevar, también solo con la decisión: un objeto sobra si sin él se llega al mismo valor.
inline std::vector<std::size_t> knapsack_items_by_search(const std::vector<Item>& items, Number capacity) {
    int calls = 0;
    const Number goal = knapsack_optimum_by_search(items, capacity, calls);
    std::vector<Item> kept = items;
    std::vector<std::size_t> chosen;
    Number used_value = 0;
    Number room = capacity;
    for (std::size_t i = 0; i < items.size(); i++) {
        Item current = kept[i];
        kept[i] = {0, 0};
        if (!knapsack_decide({kept, room, goal - used_value})) {
            chosen.push_back(i);
            used_value += current.value;
            room -= current.weight;
        }
    }
    return chosen;
}