// Sudoku con un solucionador SAT. Ustedes completan encode y decode. El resto lo hace driver.h.
#include <string>

#include "driver.h"

namespace {

// Escribe en out la fórmula del sudoku s, en formato DIMACS, con una variable por cada (fila, columna, dígito).
// s.k es el lado de una caja, s.n = s.k · s.k es el lado del tablero, y s.cells[fila][columna] vale 0 si está vacía.
void encode(const Sudoku& s, std::ostream& out) {
    // Por ahora, una fórmula sin ninguna cláusula: el encabezado es correcto, y no dice nada del sudoku.
    const long long variables = 1LL * s.n * s.n * s.n;
    out << "p cnf " << variables << " 0\n";
}

// Lee la respuesta de minisat de result y escribe en out el tablero resuelto, o la palabra imposible.
void decode(const Sudoku& s, std::istream& result, std::ostream& out) {
    std::string verdict;
    result >> verdict;
    (void)s;
    out << "pendiente\n";
}

}  // namespace

int main(int argc, char** argv) {
    return run_sudoku(argc, argv, encode, decode);
}