// Cuánto le cuesta a minisat el principio del palomar: n + 1 palomas en n huecos. No tiene solución, y para saberlo
// el solucionador acumula conflictos muy rápido. Tiempo: lo que informa minisat, con un límite de CPU por fórmula.
#include <iomanip>
#include <iostream>
#include <sstream>
#include <string>

#include "minisat.h"

namespace {

Cnf pigeonhole(int holes) {
    const int pigeons = holes + 1;
    Cnf formula;
    formula.variables = pigeons * holes;
    auto var = [&](int pigeon, int hole) { return pigeon * holes + hole + 1; };
    std::vector<int> vars;
    for (int p = 0; p < pigeons; p++) {
        vars.clear();
        for (int h = 0; h < holes; h++) vars.push_back(var(p, h));
        add_at_least_one(formula, vars);
    }
    for (int h = 0; h < holes; h++) {
        vars.clear();
        for (int p = 0; p < pigeons; p++) vars.push_back(var(p, h));
        add_at_most_one(formula, vars);
    }
    return formula;
}

// Busca "palabra : valor" en lo que escribe minisat.
std::string statistic(const std::string& log, const std::string& word) {
    std::istringstream in(log);
    std::string line;
    while (std::getline(in, line)) {
        if (line.rfind(word, 0) == 0) {
            std::istringstream fields(line.substr(line.find(':') + 1));
            std::string value;
            fields >> value;
            return value;
        }
    }
    return "?";
}

}  // namespace

int main() {
    std::cout << "huecos  variables  cláusulas  respuesta  conflictos  CPU (s)\n";
    for (int holes = 5; holes <= 12; holes++) {
        Cnf formula = pigeonhole(holes);
        SatResult result;
        try {
            result = run_minisat(formula, "-verb=1 -cpu-lim=20");
        } catch (const std::exception&) {
            // minisat termina con 0 cuando se le acaba el límite: no sabe la respuesta.
            std::cout << std::setw(6) << holes << "  se acabó el límite de 20 s de CPU\n";
            break;
        }
        std::cout << std::setw(6) << holes << std::setw(11) << formula.variables << std::setw(11)
                  << formula.clauses.size() << std::setw(11) << (result.satisfiable ? "SAT" : "UNSAT") << std::setw(12)
                  << statistic(result.statistics, "conflicts") << std::setw(9)
                  << statistic(result.statistics, "CPU time") << '\n';
    }
}