// Backtracking por filas, para comparar con el solucionador SAT en el laboratorio. Lee un sudoku de 9 por 9 de un
// archivo, en el formato de Introducción a la Programación: 9 líneas de 9 dígitos, con 0 en las celdas vacías. Sin
// archivo, usa uno de 17 valores dados, difícil para este orden de búsqueda. Solo informa nodos y tiempo.
#include <array>
#include <chrono>
#include <fstream>
#include <iostream>
#include <string>
#include <vector>

namespace {

using Grid = std::array<int, 81>;

const char* const hard_puzzle[] = {"000000000", "000003085", "001020000", "000507000", "004000100",
                                   "090000000", "500000073", "002010000", "000040009"};

struct Counter {
    long long nodes = 0;
};

bool can_place(const Grid& grid, int position, int digit) {
    const int r = position / 9, c = position % 9;
    for (int i = 0; i < 9; i++) {
        if (grid[r * 9 + i] == digit || grid[i * 9 + c] == digit) return false;
        if (grid[(r / 3 * 3 + i / 3) * 9 + c / 3 * 3 + i % 3] == digit) return false;
    }
    return true;
}

bool solve(Grid& grid, int position, Counter& counter) {
    counter.nodes++;
    while (position < 81 && grid[position] != 0) position++;
    if (position == 81) return true;
    for (int digit = 1; digit <= 9; digit++) {
        if (can_place(grid, position, digit)) {
            grid[position] = digit;
            if (solve(grid, position + 1, counter)) return true;
            grid[position] = 0;
        }
    }
    return false;
}

}  // namespace

int main(int argc, char** argv) {
    std::vector<std::string> lines;
    if (argc > 1) {
        std::ifstream in(argv[1]);
        std::string line;
        while (in >> line) lines.push_back(line);
    } else {
        lines.assign(std::begin(hard_puzzle), std::end(hard_puzzle));
    }
    Grid grid{};
    int given = 0;
    for (int i = 0; i < 81; i++) {
        grid[i] = lines.at(i / 9).at(i % 9) - '0';
        given += grid[i] != 0 ? 1 : 0;
    }
    Counter counter;
    const auto start = std::chrono::steady_clock::now();
    const bool solved = solve(grid, 0, counter);
    const std::chrono::duration<double> elapsed = std::chrono::steady_clock::now() - start;
    std::cout << "valores dados: " << given << "\n";
    std::cout << "resultado: " << (solved ? "tiene solución" : "sin solución") << "\n";
    std::cout << "nodos: " << counter.nodes << "\n";
    std::cout << "segundos: " << elapsed.count() << "\n";
}

// CNF a mano: "exactamente uno de x, y, z" con su tabla de verdad, y un DPLL seguido paso a paso.
#include <iostream>

#include "cnf.h"

int main() {
    Cnf one;
    one.variables = 3;
    add_exactly_one(one, {1, 2, 3});
    std::cout << "Exactamente uno de x, y, z. Las variables son 1, 2 y 3:\n" << one.to_dimacs();
    std::cout << "\nx y z  fórmula  verdaderas\n";
    for (int mask = 0; mask < 8; mask++) {
        Assignment value{false, (mask & 4) != 0, (mask & 2) != 0, (mask & 1) != 0};
        std::cout << value[1] << ' ' << value[2] << ' ' << value[3] << "  " << satisfies(one, value) << "        "
                  << value[1] + value[2] + value[3] << '\n';
    }

    Cnf formula;
    formula.variables = 4;
    formula.add({1, 2});
    formula.add({-1, 3});
    formula.add({-1, -3});
    formula.add({-2, 4});
    std::cout << "\nDPLL con (1 ∨ 2) ∧ (¬1 ∨ 3) ∧ (¬1 ∨ ¬3) ∧ (¬2 ∨ 4):\n";
    Dpll solver(formula, &std::cout);
    bool sat = solver.solve();
    std::cout << (sat ? "satisfacible:" : "insatisfacible");
    if (sat) {
        for (int v = 1; v <= formula.variables; v++) std::cout << ' ' << (solver.value(v) ? v : -v);
    }
    std::cout << '\n';
}

// Fórmulas en CNF. Las variables van de 1 a variables, y un literal negativo es la variable negada,
// igual que en DIMACS.
#ifndef CNF_H
#define CNF_H

#include <cstdlib>
#include <ostream>
#include <sstream>
#include <string>
#include <vector>

using Clause = std::vector<int>;

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

    void add(Clause clause) { clauses.push_back(std::move(clause)); }

    std::string to_dimacs() const {
        std::ostringstream out;
        out << "p cnf " << variables << ' ' << clauses.size() << '\n';
        for (const Clause& clause : clauses) {
            for (int literal : clause) out << literal << ' ';
            out << "0\n";
        }
        return out.str();
    }
};

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

inline bool literal_true(int literal, const Assignment& value) {
    return literal > 0 ? value[literal] : !value[-literal];
}

// El verificador de SAT: el certificado es la asignación, y se mira cada literal una vez.
inline bool satisfies(const Cnf& formula, const Assignment& value) {
    for (const Clause& clause : formula.clauses) {
        bool any = false;
        for (int literal : clause) any = any || literal_true(literal, value);
        if (!any) return false;
    }
    return true;
}

// Reglas sobre una lista de variables.
inline void add_at_least_one(Cnf& formula, const std::vector<int>& vars) { formula.add(vars); }

inline void add_at_most_one(Cnf& formula, const std::vector<int>& vars) {
    for (std::size_t i = 0; i < vars.size(); i++) {
        for (std::size_t j = i + 1; j < vars.size(); j++) formula.add({-vars[i], -vars[j]});
    }
}

inline void add_exactly_one(Cnf& formula, const std::vector<int>& vars) {
    add_at_least_one(formula, vars);
    add_at_most_one(formula, vars);
}

// Fuerza bruta: las 2^variables asignaciones. Llama a visit con cada una que satisface.
template <typename Visit>
long long for_each_model(const Cnf& formula, Visit visit) {
    long long models = 0;
    const long long total = 1LL << formula.variables;
    Assignment value(formula.variables + 1, false);
    for (long long mask = 0; mask < total; mask++) {
        for (int v = 1; v <= formula.variables; v++) value[v] = ((mask >> (v - 1)) & 1) != 0;
        if (satisfies(formula, value)) {
            models++;
            visit(value);
        }
    }
    return models;
}

inline long long count_models(const Cnf& formula) {
    return for_each_model(formula, [](const Assignment&) {});
}

// DPLL: propagar cláusulas unitarias y, si no hay ninguna, probar una variable con los dos valores.
// state[v]: 0 sin asignar, 1 verdadera, −1 falsa. Si se pasa trace, anota lo que va pasando.
class Dpll {
public:
    explicit Dpll(const Cnf& formula, std::ostream* trace = nullptr)
        : formula_(formula), trace_(trace), state_(formula.variables + 1, 0) {}

    bool solve() { return search(0); }

    bool value(int v) const { return state_[v] == 1; }
    long long decisions() const { return decisions_; }

private:
    const Cnf& formula_;
    std::ostream* trace_;
    std::vector<int> state_;
    long long decisions_ = 0;

    void note(int depth, const std::string& text) {
        if (trace_ != nullptr) *trace_ << std::string(2 * static_cast<std::size_t>(depth), ' ') << text << '\n';
    }

    // Devuelve false si alguna cláusula queda con todos sus literales falsos.
    bool propagate(int depth, std::vector<int>& assigned) {
        bool changed = true;
        while (changed) {
            changed = false;
            for (const Clause& clause : formula_.clauses) {
                int free_literal = 0, free_count = 0;
                bool is_true = false;
                for (int literal : clause) {
                    int s = state_[std::abs(literal)];
                    if (s == 0) {
                        free_literal = literal;
                        free_count++;
                    } else if ((s == 1) == (literal > 0)) {
                        is_true = true;
                    }
                }
                if (is_true) continue;
                if (free_count == 0) {
                    note(depth, "conflicto");
                    return false;
                }
                if (free_count == 1) {
                    state_[std::abs(free_literal)] = free_literal > 0 ? 1 : -1;
                    assigned.push_back(std::abs(free_literal));
                    note(depth, "unitaria: " + std::to_string(free_literal));
                    changed = true;
                }
            }
        }
        return true;
    }

    bool search(int depth) {
        std::vector<int> assigned;
        bool ok = propagate(depth, assigned);
        if (ok) {
            int v = 1;
            while (v <= formula_.variables && state_[v] != 0) v++;
            if (v > formula_.variables) return true;
            for (int s : {1, -1}) {
                decisions_++;
                note(depth, "decisión: " + std::to_string(s * v));
                state_[v] = s;
                if (search(depth + 1)) return true;
                state_[v] = 0;
            }
        }
        for (int v : assigned) state_[v] = 0;
        return false;
    }
};

#endif

// Coloreo con minisat: la fórmula en DIMACS, la respuesta tal cual y su lectura.
#include <iostream>

#include "coloring.h"
#include "minisat.h"

namespace {

void solve_and_print(const std::string& name, const Graph& g, int colors, bool at_most_one) {
    Cnf formula = encode_coloring(g, colors, at_most_one);
    SatResult result = run_minisat(formula);
    std::cout << name << " con " << colors << " colores: " << formula.variables << " variables, "
              << formula.clauses.size() << " cláusulas, código " << result.exit_code << ": ";
    if (!result.satisfiable) {
        std::cout << "no se puede\n";
        return;
    }
    std::vector<int> color = decode_coloring(g, colors, result.value);
    for (int c : color) std::cout << c << ' ';
    std::cout << (is_proper_coloring(g, color) ? "(propio)\n" : "(NO propio)\n");
}

}  // namespace

int main() {
    const Graph triangle{3, {{0, 1}, {1, 2}, {0, 2}}};
    Cnf formula = encode_coloring(triangle, 3, true);
    std::cout << "El triángulo con 3 colores. Variable v · 3 + c + 1 para el nodo v y el color c:\n";
    std::cout << formula.to_dimacs();
    SatResult result = run_minisat(formula);
    std::cout << "\nminisat terminó con el código " << result.exit_code << ". El archivo de respuesta dice:\n"
              << result.raw;

    SatResult no = run_minisat(encode_coloring(triangle, 2, true));
    std::cout << "\nCon 2 colores, minisat terminó con el código " << no.exit_code << ". El archivo dice:\n"
              << no.raw << '\n';

    const Graph pentagon{5, {{0, 1}, {1, 2}, {2, 3}, {3, 4}, {4, 0}}};
    const Graph k4{4, {{0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 3}, {2, 3}}};
    const Graph petersen{10, {{0, 1}, {1, 2}, {2, 3}, {3, 4}, {4, 0}, {5, 7}, {7, 9}, {9, 6},
                              {6, 8}, {8, 5}, {0, 5}, {1, 6}, {2, 7}, {3, 8}, {4, 9}}};
    solve_and_print("ciclo de 5", pentagon, 2, true);
    solve_and_print("ciclo de 5", pentagon, 3, true);
    solve_and_print("K4", k4, 3, true);
    solve_and_print("K4", k4, 4, true);
    solve_and_print("Petersen", petersen, 2, true);
    solve_and_print("Petersen", petersen, 3, true);

    std::cout << "\nSin \"a lo sumo un color por nodo\":\n";
    solve_and_print("Petersen", petersen, 3, false);
    const Graph edge{2, {{0, 1}}};
    Cnf loose = encode_coloring(edge, 3, false), strict = encode_coloring(edge, 3, true);
    std::cout << "Una arista con 3 colores tiene " << count_models(strict) << " modelos con la regla y "
              << count_models(loose) << " sin ella.\n";
    int shown = 0;
    long long proper = 0, total = 0;
    for_each_model(loose, [&](const Assignment& value) {
        total++;
        // Cualquier color verdadero sirve: se prueban todas las elecciones posibles.
        bool every_choice = true;
        for (int a = 0; a < 3; a++) {
            for (int b = 0; b < 3; b++) {
                if (value[color_variable(0, a, 3)] && value[color_variable(1, b, 3)] && a == b) every_choice = false;
            }
        }
        proper += every_choice;
        std::vector<int> count = true_colors(edge, 3, value);
        if (shown == 0 && (count[0] > 1 || count[1] > 1)) {
            shown++;
            std::cout << "Un modelo con dos colores en un nodo:";
            for (int v = 0; v < 2; v++) {
                std::cout << " nodo " << v << " = {";
                for (int c = 0; c < 3; c++) {
                    if (value[color_variable(v, c, 3)]) std::cout << ' ' << c;
                }
                std::cout << " }";
            }
            std::cout << '\n';
        }
    });
    std::cout << "De " << total << " modelos sin la regla, en " << proper << " cualquier elección da un coloreo propio.\n";
}

// Coloreo de grafos como CNF: una variable por cada (nodo, color).
#ifndef COLORING_H
#define COLORING_H

#include <vector>

#include "cnf.h"
#include "graphs.h"

inline int color_variable(int node, int color, int colors) { return node * colors + color + 1; }

// Cada nodo tiene al menos un color, y dos vecinos no comparten ninguno. "A lo sumo un color por nodo" es opcional.
inline Cnf encode_coloring(const Graph& g, int colors, bool at_most_one) {
    Cnf formula;
    formula.variables = g.n * colors;
    std::vector<int> vars(colors);
    for (int v = 0; v < g.n; v++) {
        for (int c = 0; c < colors; c++) vars[c] = color_variable(v, c, colors);
        add_at_least_one(formula, vars);
        if (at_most_one) add_at_most_one(formula, vars);
    }
    for (auto [u, v] : g.edges) {
        for (int c = 0; c < colors; c++) formula.add({-color_variable(u, c, colors), -color_variable(v, c, colors)});
    }
    return formula;
}

// Lee el primer color verdadero de cada nodo.
inline std::vector<int> decode_coloring(const Graph& g, int colors, const Assignment& value) {
    std::vector<int> color(g.n, -1);
    for (int v = 0; v < g.n; v++) {
        for (int c = colors - 1; c >= 0; c--) {
            if (value[color_variable(v, c, colors)]) color[v] = c;
        }
    }
    return color;
}

// Cuántos colores verdaderos tiene cada nodo.
inline std::vector<int> true_colors(const Graph& g, int colors, const Assignment& value) {
    std::vector<int> count(g.n, 0);
    for (int v = 0; v < g.n; v++) {
        for (int c = 0; c < colors; c++) count[v] += value[color_variable(v, c, colors)] ? 1 : 0;
    }
    return count;
}

#endif

// Grafos pequeños y las fuerzas brutas de la semana. Un conjunto de nodos es una máscara de bits.
#ifndef GRAPHS_H
#define GRAPHS_H

#include <bit>
#include <queue>
#include <string>
#include <utility>
#include <vector>

// Grafo no dirigido y simple: sin lazos y sin aristas repetidas.
struct Graph {
    int n = 0;
    std::vector<std::pair<int, int>> edges;

    bool adjacent(int u, int v) const {
        for (auto [a, b] : edges) {
            if ((a == u && b == v) || (a == v && b == u)) return true;
        }
        return false;
    }
};

// Una instancia de un problema de decisión sobre grafos: ¿hay un conjunto de tamaño k?
struct Instance {
    Graph graph;
    int k = 0;
};

inline bool contains(unsigned set, int v) { return ((set >> v) & 1u) != 0; }

// Verificadores: reciben el certificado, y solo miran cada arista una vez. Cuestan O(V + E).
inline bool is_independent_set(const Graph& g, unsigned set) {
    for (auto [u, v] : g.edges) {
        if (contains(set, u) && contains(set, v)) return false;
    }
    return true;
}

inline bool is_vertex_cover(const Graph& g, unsigned set) {
    for (auto [u, v] : g.edges) {
        if (!contains(set, u) && !contains(set, v)) return false;
    }
    return true;
}

// Mira cada par de nodos: O(V² · E) con esta representación tan simple, y O(V²) con una matriz.
inline bool is_clique(const Graph& g, unsigned set) {
    for (int u = 0; u < g.n; u++) {
        for (int v = u + 1; v < g.n; v++) {
            if (contains(set, u) && contains(set, v) && !g.adjacent(u, v)) return false;
        }
    }
    return true;
}

inline bool is_proper_coloring(const Graph& g, const std::vector<int>& color) {
    for (auto [u, v] : g.edges) {
        if (color[u] == color[v]) return false;
    }
    return true;
}

// Fuerza bruta: las 2ⁿ máscaras.
template <typename Check, typename Size>
bool any_set(const Graph& g, Check check, Size size_ok) {
    const unsigned total = 1u << g.n;
    for (unsigned set = 0; set < total; set++) {
        if (size_ok(std::popcount(set)) && check(g, set)) return true;
    }
    return false;
}

// ¿Hay un conjunto independiente de tamaño al menos k?
inline bool has_independent_set(const Instance& in) {
    return any_set(in.graph, is_independent_set, [&](int size) { return size >= in.k; });
}

// ¿Hay una cobertura de vértices de tamaño a lo sumo k?
inline bool has_vertex_cover(const Instance& in) {
    return any_set(in.graph, is_vertex_cover, [&](int size) { return size <= in.k; });
}

// ¿Hay un clique de tamaño al menos k?
inline bool has_clique(const Instance& in) {
    return any_set(in.graph, is_clique, [&](int size) { return size >= in.k; });
}

inline Graph complement(const Graph& g) {
    Graph h{g.n, {}};
    for (int u = 0; u < g.n; u++) {
        for (int v = u + 1; v < g.n; v++) {
            if (!g.adjacent(u, v)) h.edges.emplace_back(u, v);
        }
    }
    return h;
}

// Las reducciones de los apuntes. Ninguna mira si la respuesta es sí o no.
inline Instance independent_set_to_vertex_cover(const Instance& in) { return {in.graph, in.graph.n - in.k}; }
inline Instance independent_set_to_clique(const Instance& in) { return {complement(in.graph), in.k}; }
inline Instance vertex_cover_to_clique(const Instance& in) {
    return independent_set_to_clique(independent_set_to_vertex_cover(in));
}

// El grafo con un nodo nuevo, vecino de todos.
inline Graph add_apex(const Graph& g) {
    Graph h = g;
    for (int v = 0; v < g.n; v++) h.edges.emplace_back(v, g.n);
    h.n = g.n + 1;
    return h;
}

// 2-coloreo con BFS, en O(V + E) con listas de adyacencia: cada componente se pinta por capas.
inline bool two_colorable(const Graph& g) {
    std::vector<std::vector<int>> next(g.n);
    for (auto [u, v] : g.edges) {
        next[u].push_back(v);
        next[v].push_back(u);
    }
    std::vector<int> color(g.n, -1);
    for (int start = 0; start < g.n; start++) {
        if (color[start] != -1) continue;
        color[start] = 0;
        std::queue<int> pending;
        pending.push(start);
        while (!pending.empty()) {
            int u = pending.front();
            pending.pop();
            for (int v : next[u]) {
                if (color[v] == -1) {
                    color[v] = 1 - color[u];
                    pending.push(v);
                } else if (color[v] == color[u]) {
                    return false;
                }
            }
        }
    }
    return true;
}

// Fuerza bruta: prueba las colorsⁿ formas de pintar.
inline bool colorable_brute_force(const Graph& g, int colors) {
    std::vector<int> color(g.n, 0);
    while (true) {
        if (is_proper_coloring(g, color)) return true;
        int v = 0;
        while (v < g.n && ++color[v] == colors) color[v++] = 0;
        if (v == g.n) return false;
    }
}

inline std::string set_to_string(unsigned set, int n) {
    std::string text = "{";
    for (int v = 0; v < n; v++) {
        if (contains(set, v)) text += (text.size() > 1 ? ", " : "") + std::to_string(v);
    }
    return text + "}";
}

#endif

// "Al menos uno" sin "a lo sumo uno", en cuadrados latinos. Se muestran los tres casos: la regla es redundante,
// o su falta rompe la respuesta.
#include <iostream>

#include "latin.h"
#include "minisat.h"

namespace {

void print_table(const std::vector<std::vector<int>>& table) {
    for (const auto& row : table) {
        std::cout << "  ";
        for (int s : row) std::cout << s + 1 << ' ';
        std::cout << '\n';
    }
}

void solve_and_print(const std::string& name, int n, const std::vector<Given>& givens, const LatinRules& rules) {
    Cnf formula = encode_latin(n, givens, rules);
    SatResult result = run_minisat(formula);
    std::cout << name << ": " << formula.variables << " variables, " << formula.clauses.size() << " cláusulas, minisat "
              << (result.satisfiable ? "dice SAT\n" : "dice UNSAT\n");
    if (!result.satisfiable) return;
    auto table = decode_latin(n, result.value);
    print_table(table);
    std::cout << (is_latin(table) ? "  es un cuadrado latino\n" : "  NO es un cuadrado latino\n");
}

}  // namespace

int main() {
    const LatinRules complete;
    LatinRules at_least_only;
    at_least_only.cell_at_most_one = false;
    at_least_only.line_at_most_one = false;
    LatinRules no_cell_rule;
    no_cell_rule.cell_at_most_one = false;
    no_cell_rule.line_at_least_one = false;

    std::cout << "Cuántas soluciones tiene el cuadrado de lado 2:\n";
    std::cout << "  reglas completas:                      " << count_models(encode_latin(2, {}, complete)) << '\n';
    std::cout << "  celda al menos uno, línea a lo sumo uno: " << count_models(encode_latin(2, {}, no_cell_rule)) << '\n';
    std::cout << "  solo reglas de al menos uno:           " << count_models(encode_latin(2, {}, at_least_only)) << '\n';

    std::cout << "\nEl argumento del palomar, en una fila de n celdas (todas las asignaciones):\n";
    for (int n = 2; n <= 4; n++) {
        Cnf row = one_row_formula(n);
        long long two_in_a_cell = 0;
        long long models = for_each_model(row, [&](const Assignment& value) {
            for (int cell = 0; cell < n; cell++) {
                int count = 0;
                for (int s = 0; s < n; s++) count += value[cell * n + s + 1] ? 1 : 0;
                if (count > 1) {
                    two_in_a_cell++;
                    return;
                }
            }
        });
        std::cout << "  n = " << n << ": " << models << " modelos, " << two_in_a_cell << " con dos símbolos en una celda\n";
    }

    std::cout << "\nUn cuadrado de lado 3, con 1 en la celda (0, 0) y 2 en la celda (1, 1):\n";
    const std::vector<Given> fine{{0, 0, 0}, {1, 1, 1}};
    solve_and_print("reglas completas", 3, fine, complete);
    solve_and_print("celda al menos uno, línea a lo sumo uno", 3, fine, no_cell_rule);
    solve_and_print("solo al menos uno", 3, fine, at_least_only);

    std::cout << "\nEl mismo cuadrado con 1 en (0, 0) y 1 en (0, 1), que no tiene solución:\n";
    const std::vector<Given> clash{{0, 0, 0}, {0, 1, 0}};
    solve_and_print("reglas completas", 3, clash, complete);
    solve_and_print("celda al menos uno, línea a lo sumo uno", 3, clash, no_cell_rule);
    solve_and_print("solo al menos uno", 3, clash, at_least_only);
}

// Cuadrado latino de lado n: una tabla donde cada fila y cada columna tiene cada símbolo una vez.
// Una variable por cada (fila, columna, símbolo). Sirve para ver qué pasa con "al menos uno" y "a lo sumo uno".
#ifndef LATIN_H
#define LATIN_H

#include <vector>

#include "cnf.h"

struct LatinRules {
    bool cell_at_least_one = true;
    bool cell_at_most_one = true;
    bool line_at_least_one = true;   // cada símbolo sale en cada fila y en cada columna
    bool line_at_most_one = true;    // cada símbolo no se repite en una fila ni en una columna
};

inline int latin_variable(int n, int row, int column, int symbol) { return row * n * n + column * n + symbol + 1; }

struct Given {
    int row, column, symbol;
};

inline Cnf encode_latin(int n, const std::vector<Given>& givens, const LatinRules& rules) {
    Cnf formula;
    formula.variables = n * n * n;
    std::vector<int> vars(n);
    auto apply = [&](bool least, bool most) {
        if (least) add_at_least_one(formula, vars);
        if (most) add_at_most_one(formula, vars);
    };
    for (int a = 0; a < n; a++) {
        for (int b = 0; b < n; b++) {
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, a, b, x);
            apply(rules.cell_at_least_one, rules.cell_at_most_one);
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, a, x, b);
            apply(rules.line_at_least_one, rules.line_at_most_one);
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, x, a, b);
            apply(rules.line_at_least_one, rules.line_at_most_one);
        }
    }
    for (const Given& g : givens) formula.add({latin_variable(n, g.row, g.column, g.symbol)});
    return formula;
}

// Lee el primer símbolo verdadero de cada celda.
inline std::vector<std::vector<int>> decode_latin(int n, const Assignment& value) {
    std::vector<std::vector<int>> table(n, std::vector<int>(n, -1));
    for (int r = 0; r < n; r++) {
        for (int c = 0; c < n; c++) {
            for (int s = n - 1; s >= 0; s--) {
                if (value[latin_variable(n, r, c, s)]) table[r][c] = s;
            }
        }
    }
    return table;
}

inline bool is_latin(const std::vector<std::vector<int>>& table) {
    const int n = static_cast<int>(table.size());
    for (int a = 0; a < n; a++) {
        std::vector<int> in_row(n, 0), in_column(n, 0);
        for (int b = 0; b < n; b++) {
            if (table[a][b] < 0 || table[b][a] < 0) return false;
            if (in_row[table[a][b]]++ || in_column[table[b][a]]++) return false;
        }
    }
    return true;
}

// Una sola fila de n celdas: al menos un símbolo por celda, y cada símbolo a lo sumo una vez en la fila.
// Es la situación del argumento del palomar.
inline Cnf one_row_formula(int n) {
    Cnf formula;
    formula.variables = n * n;
    auto var = [&](int cell, int symbol) { return cell * n + symbol + 1; };
    std::vector<int> vars(n);
    for (int a = 0; a < n; a++) {
        for (int x = 0; x < n; x++) vars[x] = var(a, x);
        add_at_least_one(formula, vars);
        for (int x = 0; x < n; x++) vars[x] = var(x, a);
        add_at_most_one(formula, vars);
    }
    return formula;
}

#endif

// Correr minisat desde C++: se escribe la fórmula en un archivo, se llama al programa y se lee su respuesta.
// mkdtemp y WEXITSTATUS no son C++ estándar: son de POSIX, y el entorno del curso los tiene.
#ifndef MINISAT_H
#define MINISAT_H

#include <cstdlib>
#include <filesystem>
#include <fstream>
#include <stdexcept>
#include <string>
#include <vector>

#include <sys/wait.h>
#include <unistd.h>

#include "cnf.h"

struct SatResult {
    bool satisfiable = false;
    int exit_code = 0;
    Assignment value;       // si satisfiable; una variable que no sale en la respuesta queda falsa
    std::string raw;        // el archivo de respuesta, tal cual
    std::string statistics; // lo que minisat escribe en la terminal
};

inline SatResult run_minisat(const Cnf& formula, const std::string& options = "-verb=0") {
    std::string pattern = (std::filesystem::temp_directory_path() / "week13_XXXXXX").string();
    if (mkdtemp(pattern.data()) == nullptr) throw std::runtime_error("no se pudo crear la carpeta temporal");
    const std::filesystem::path folder = pattern;
    {
        std::ofstream cnf(folder / "formula.cnf");
        cnf << formula.to_dimacs();
    }
    const std::string command = "minisat " + options + " '" + (folder / "formula.cnf").string() + "' '" +
                                (folder / "result.txt").string() + "' > '" + (folder / "log.txt").string() + "' 2>&1";
    int status = std::system(command.c_str());

    SatResult result;
    result.exit_code = WIFEXITED(status) ? WEXITSTATUS(status) : -1;
    auto slurp = [](const std::filesystem::path& path) {
        std::ifstream in(path);
        std::ostringstream all;
        all << in.rdbuf();
        return all.str();
    };
    result.raw = slurp(folder / "result.txt");
    result.statistics = slurp(folder / "log.txt");
    std::filesystem::remove_all(folder);
    if (result.exit_code != 10 && result.exit_code != 20) {
        throw std::runtime_error("minisat terminó con el código " + std::to_string(result.exit_code));
    }

    result.satisfiable = result.exit_code == 10;
    result.value.assign(formula.variables + 1, false);
    if (result.satisfiable) {
        std::istringstream in(result.raw);
        std::string verdict;
        in >> verdict;
        int literal;
        while (in >> literal && literal != 0) {
            if (literal > 0) result.value[literal] = true;
        }
    }
    return result;
}

#endif

// Las tres reducciones en un grafo pequeño, comparadas con fuerza bruta, y una reducción mal hecha.
#include <iostream>

#include "graphs.h"

namespace {

Graph small_graph() {
    return {6, {{0, 1}, {0, 2}, {1, 2}, {2, 3}, {3, 4}, {4, 5}}};
}

void print_edges(const Graph& g) {
    for (auto [u, v] : g.edges) std::cout << ' ' << u << '-' << v;
    std::cout << '\n';
}

std::string yes_no(bool answer) { return answer ? "sí" : "no"; }

// Busca el conjunto más grande que cumple check, entre todas las máscaras.
template <typename Check>
unsigned best_set(const Graph& g, Check check, bool largest) {
    unsigned best = 0;
    bool found = false;
    for (unsigned set = 0; set < (1u << g.n); set++) {
        if (!check(g, set)) continue;
        int size = std::popcount(set), size_best = std::popcount(best);
        if (!found || (largest ? size > size_best : size < size_best)) best = set;
        found = true;
    }
    return best;
}

// Recorre los grafos de menos a más nodos, hasta que CI(G, k) y CV(G, k) no coinciden.
void print_counterexample() {
    for (int n = 1; n <= 4; n++) {
        for (unsigned edges = 0; edges < (1u << (n * (n - 1) / 2)); edges++) {
            Graph candidate{n, {}};
            int bit = 0;
            for (int u = 0; u < n; u++) {
                for (int v = u + 1; v < n; v++) {
                    if ((edges >> bit++) & 1u) candidate.edges.emplace_back(u, v);
                }
            }
            for (int k = 1; k <= n; k++) {
                Instance in{candidate, k};
                if (has_independent_set(in) != has_vertex_cover(in)) {
                    std::cout << "  el contraejemplo más chico: " << n << " nodos, aristas:";
                    print_edges(candidate);
                    std::cout << "  k = " << k << ": CI dice " << yes_no(has_independent_set(in)) << ", CV dice "
                              << yes_no(has_vertex_cover(in)) << '\n';
                    return;
                }
            }
        }
    }
}

}  // namespace

int main() {
    const Graph g = small_graph();
    std::cout << "G tiene " << g.n << " nodos y estas aristas:";
    print_edges(g);
    unsigned independent = best_set(g, is_independent_set, true);
    unsigned cover = best_set(g, is_vertex_cover, false);
    std::cout << "conjunto independiente máximo: " << set_to_string(independent, g.n) << ", tamaño "
              << std::popcount(independent) << '\n';
    std::cout << "cobertura mínima:              " << set_to_string(cover, g.n) << ", tamaño " << std::popcount(cover)
              << '\n';
    const unsigned rest = ((1u << g.n) - 1) & ~independent;
    std::cout << "V − S = " << set_to_string(rest, g.n) << ", ¿es cobertura? " << yes_no(is_vertex_cover(g, rest))
              << '\n';

    std::cout << "\nConjunto independiente a cobertura, con k → n − k:\n";
    std::cout << "  k  CI(G, k)  CV(G, n − k)\n";
    for (int k = 0; k <= g.n + 1; k++) {
        Instance in{g, k};
        std::cout << "  " << k << "  " << yes_no(has_independent_set(in)) << "        "
                  << yes_no(has_vertex_cover(independent_set_to_vertex_cover(in))) << '\n';
    }

    const Graph h = complement(g);
    std::cout << "\nEl complemento tiene estas aristas:";
    print_edges(h);
    unsigned clique = best_set(h, is_clique, true);
    std::cout << "clique máximo del complemento: " << set_to_string(clique, g.n) << ", tamaño "
              << std::popcount(clique) << '\n';
    std::cout << "  k  CI(G, k)  clique(complemento, k)\n";
    for (int k = 0; k <= g.n + 1; k++) {
        Instance in{g, k};
        std::cout << "  " << k << "  " << yes_no(has_independent_set(in)) << "        "
                  << yes_no(has_clique(independent_set_to_clique(in))) << '\n';
    }

    std::cout << "\nUna reducción mal hecha: conservar k, sin cambiarlo por n − k.\n";
    print_counterexample();

    std::cout << "\n2-coloreo a 3-coloreo: agregar un nodo vecino de todos.\n";
    const Graph pentagon{5, {{0, 1}, {1, 2}, {2, 3}, {3, 4}, {4, 0}}};
    const Graph square{4, {{0, 1}, {1, 2}, {2, 3}, {3, 0}}};
    for (const auto& [name, graph] : {std::pair{"ciclo de 4", square}, std::pair{"ciclo de 5", pentagon}}) {
        std::cout << "  " << name << ": 2 colores con BFS: " << yes_no(two_colorable(graph))
                  << "; 3 colores en el grafo con el nodo nuevo: " << yes_no(colorable_brute_force(add_apex(graph), 3))
                  << '\n';
    }
}