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