// 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";
}