// 2-SAT: el grafo de implicaciones, las componentes y la asignación que sale de ellas.
#include <iostream>
#include "two_sat.h"

namespace {

void solve(int variables, const std::vector<TwoClause>& clauses) {
    Formula f = two_clauses_as_formula(variables, clauses);
    std::cout << formula_text(f) << '\n';
    ImplicationGraph g = implication_graph(variables, clauses);
    std::cout << "  aristas:";
    for (std::size_t u = 0; u < g.size(); u++) {
        for (int v : g[u]) std::cout << ' ' << literal_text(two_sat_literal(u)) << "→" << literal_text(two_sat_literal(static_cast<std::size_t>(v)));
    }
    std::cout << '\n';
    std::vector<int> comp = implication_components(g);
    std::cout << "  componentes, en el orden en que salen (de sumidero a fuente):";
    int count = 0;
    for (int c : comp) count = std::max(count, c + 1);
    for (int c = 0; c < count; c++) {
        std::cout << " {";
        bool first = true;
        for (std::size_t node = 0; node < comp.size(); node++) {
            if (comp[node] == c) {
                std::cout << (first ? "" : " ") << literal_text(two_sat_literal(node));
                first = false;
            }
        }
        std::cout << "}";
    }
    std::cout << '\n';
    if (same_component_clash(comp)) {
        for (std::size_t node = 0; node < comp.size(); node += 2) {
            if (comp[node] == comp[node + 1]) std::cout << "  " << literal_text(two_sat_literal(node)) << " y su negación en la misma componente\n";
        }
        std::cout << "  insatisfacible; fuerza bruta: " << (brute_sat(f) ? "satisfacible" : "insatisfacible") << "\n\n";
        return;
    }
    Assignment a = assignment_from_components(comp);
    Assignment wrong = assignment_with_reversed_order(comp);
    std::cout << "  x verdadera si comp[x] < comp[¬x]: " << assignment_text(a) << ", ¿cumple? " << (satisfies(f, a) ? "sí" : "no") << '\n';
    std::cout << "  con el orden al revés:            " << assignment_text(wrong) << ", ¿cumple? " << (satisfies(f, wrong) ? "sí" : "no") << "\n\n";
}

}  // namespace

int main() {
    solve(3, {{1, 2}, {-1, 3}, {-2, -3}, {-3, -1}});
    solve(4, {{1, 2}, {-2, 3}, {-3, 4}});
    solve(2, {{1, 2}, {1, -2}, {-1, 2}, {-1, -2}});
    std::cout << "Cláusulas raras: (x1 ∨ x1) obliga a x1, y (x2 ∨ ¬x2) no dice nada.\n";
    solve(2, {{1, 1}, {2, -2}});

    std::vector<TwoClause> hard = {{1, 2}, {1, -2}, {-1, 2}, {-1, -2}};
    ImplicationGraph half = implication_graph(2, hard, false);
    std::cout << "Con una sola arista por cláusula, en la fórmula insatisfacible:\n";
    std::cout << "  ¿x y ¬x en la misma componente? " << (same_component_clash(implication_components(half)) ? "sí" : "no") << '\n';
}