// "Al menos uno" sin "a lo sumo uno", en cuadrados latinos. Se muestran los tres casos: la regla es redundante,
// o su falta rompe la respuesta.
#include <iostream>

#include "latin.h"
#include "minisat.h"

namespace {

void print_table(const std::vector<std::vector<int>>& table) {
    for (const auto& row : table) {
        std::cout << "  ";
        for (int s : row) std::cout << s + 1 << ' ';
        std::cout << '\n';
    }
}

void solve_and_print(const std::string& name, int n, const std::vector<Given>& givens, const LatinRules& rules) {
    Cnf formula = encode_latin(n, givens, rules);
    SatResult result = run_minisat(formula);
    std::cout << name << ": " << formula.variables << " variables, " << formula.clauses.size() << " cláusulas, minisat "
              << (result.satisfiable ? "dice SAT\n" : "dice UNSAT\n");
    if (!result.satisfiable) return;
    auto table = decode_latin(n, result.value);
    print_table(table);
    std::cout << (is_latin(table) ? "  es un cuadrado latino\n" : "  NO es un cuadrado latino\n");
}

}  // namespace

int main() {
    const LatinRules complete;
    LatinRules at_least_only;
    at_least_only.cell_at_most_one = false;
    at_least_only.line_at_most_one = false;
    LatinRules no_cell_rule;
    no_cell_rule.cell_at_most_one = false;
    no_cell_rule.line_at_least_one = false;

    std::cout << "Cuántas soluciones tiene el cuadrado de lado 2:\n";
    std::cout << "  reglas completas:                      " << count_models(encode_latin(2, {}, complete)) << '\n';
    std::cout << "  celda al menos uno, línea a lo sumo uno: " << count_models(encode_latin(2, {}, no_cell_rule)) << '\n';
    std::cout << "  solo reglas de al menos uno:           " << count_models(encode_latin(2, {}, at_least_only)) << '\n';

    std::cout << "\nEl argumento del palomar, en una fila de n celdas (todas las asignaciones):\n";
    for (int n = 2; n <= 4; n++) {
        Cnf row = one_row_formula(n);
        long long two_in_a_cell = 0;
        long long models = for_each_model(row, [&](const Assignment& value) {
            for (int cell = 0; cell < n; cell++) {
                int count = 0;
                for (int s = 0; s < n; s++) count += value[cell * n + s + 1] ? 1 : 0;
                if (count > 1) {
                    two_in_a_cell++;
                    return;
                }
            }
        });
        std::cout << "  n = " << n << ": " << models << " modelos, " << two_in_a_cell << " con dos símbolos en una celda\n";
    }

    std::cout << "\nUn cuadrado de lado 3, con 1 en la celda (0, 0) y 2 en la celda (1, 1):\n";
    const std::vector<Given> fine{{0, 0, 0}, {1, 1, 1}};
    solve_and_print("reglas completas", 3, fine, complete);
    solve_and_print("celda al menos uno, línea a lo sumo uno", 3, fine, no_cell_rule);
    solve_and_print("solo al menos uno", 3, fine, at_least_only);

    std::cout << "\nEl mismo cuadrado con 1 en (0, 0) y 1 en (0, 1), que no tiene solución:\n";
    const std::vector<Given> clash{{0, 0, 0}, {0, 1, 0}};
    solve_and_print("reglas completas", 3, clash, complete);
    solve_and_print("celda al menos uno, línea a lo sumo uno", 3, clash, no_cell_rule);
    solve_and_print("solo al menos uno", 3, clash, at_least_only);
}