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