// La reducción de SAT a 3-SAT, cláusula por cláusula, comparada con la fuerza bruta.
#include <iostream>
#include "three_sat.h"

namespace {

void show(const Formula& f) {
    Formula out = to_three_sat(f);
    std::cout << "entrada: " << formula_text(f) << '\n';
    std::cout << "salida, con " << out.variables << " variables y " << out.clauses.size() << " cláusulas:\n";
    for (const Clause& c : out.clauses) std::cout << "  " << clause_text(c) << '\n';
    if (out.clauses.empty()) std::cout << "  (ninguna)\n";
    std::cout << "  fuerza bruta: entrada " << (brute_sat(f) ? "satisfacible" : "insatisfacible") << ", salida "
              << (brute_sat(out) ? "satisfacible" : "insatisfacible") << "\n\n";
}

}  // namespace

int main() {
    std::cout << "Una cláusula larga se parte en una cadena:\n";
    show({6, {{1, 2, 3, 4, 5, 6}}});

    std::cout << "Una cláusula corta se rellena con variables nuevas:\n";
    show({1, {{1}}});
    show({2, {{1, -2}}});

    std::cout << "Repetidos y cláusulas que siempre se cumplen:\n";
    show({2, {{1, 1, -2, 1}}});
    show({2, {{1, -1, 2}}});

    std::cout << "Una fórmula sin solución sigue sin solución:\n";
    show({2, {{1}, {-1, 2}, {-2}}});

    Formula long_clause{6, {{1, 2, 3, 4, 5, 6}}};
    Formula out = to_three_sat(long_clause);
    Assignment a(7, false);
    a[4] = true;
    Assignment extended = extend_assignment(long_clause, a, out.variables);
    std::cout << "Extender x4 = V en la cadena: " << assignment_text(extended) << '\n';
    std::cout << "  (x7, x8, x9 son y1, y2, y3)\n";
    std::cout << "  ¿cumple la salida? " << (satisfies(out, extended) ? "sí" : "no") << '\n';
}