// CNF a mano: "exactamente uno de x, y, z" con su tabla de verdad, y un DPLL seguido paso a paso.
#include <iostream>

#include "cnf.h"

int main() {
    Cnf one;
    one.variables = 3;
    add_exactly_one(one, {1, 2, 3});
    std::cout << "Exactamente uno de x, y, z. Las variables son 1, 2 y 3:\n" << one.to_dimacs();
    std::cout << "\nx y z  fórmula  verdaderas\n";
    for (int mask = 0; mask < 8; mask++) {
        Assignment value{false, (mask & 4) != 0, (mask & 2) != 0, (mask & 1) != 0};
        std::cout << value[1] << ' ' << value[2] << ' ' << value[3] << "  " << satisfies(one, value) << "        "
                  << value[1] + value[2] + value[3] << '\n';
    }

    Cnf formula;
    formula.variables = 4;
    formula.add({1, 2});
    formula.add({-1, 3});
    formula.add({-1, -3});
    formula.add({-2, 4});
    std::cout << "\nDPLL con (1 ∨ 2) ∧ (¬1 ∨ 3) ∧ (¬1 ∨ ¬3) ∧ (¬2 ∨ 4):\n";
    Dpll solver(formula, &std::cout);
    bool sat = solver.solve();
    std::cout << (sat ? "satisfacible:" : "insatisfacible");
    if (sat) {
        for (int v = 1; v <= formula.variables; v++) std::cout << ' ' << (solver.value(v) ? v : -v);
    }
    std::cout << '\n';
}