// Fórmulas en CNF. Un literal es un entero: +v es la variable v, y -v es su negación. Las variables
// se numeran desde 1, como en DIMACS.
#pragma once
#include <cstddef>
#include <cstdlib>
#include <optional>
#include <string>
#include <vector>

using Clause = std::vector<int>;

struct Formula {
    int variables = 0;
    std::vector<Clause> clauses;
};

// Assignment[v] es el valor de la variable v. La posición 0 no se usa.
using Assignment = std::vector<bool>;

inline bool literal_true(const Assignment& a, int literal) {
    bool value = a[static_cast<std::size_t>(std::abs(literal))];
    return literal > 0 ? value : !value;
}

inline bool clause_true(const Assignment& a, const Clause& c) {
    for (int literal : c) {
        if (literal_true(a, literal)) return true;
    }
    return false;
}

// El verificador de SAT: el certificado es la asignación, y revisarla es lineal en la fórmula.
inline bool satisfies(const Formula& f, const Assignment& a) {
    for (const Clause& c : f.clauses) {
        if (!clause_true(a, c)) return false;
    }
    return true;
}

// Fuerza bruta: prueba las 2ⁿ asignaciones. Solo para fórmulas pequeñas.
inline std::optional<Assignment> brute_sat(const Formula& f) {
    const std::size_t n = static_cast<std::size_t>(f.variables);
    for (unsigned long long mask = 0; mask < (1ULL << n); mask++) {
        Assignment a(n + 1, false);
        for (std::size_t v = 1; v <= n; v++) a[v] = (mask >> (v - 1)) & 1;
        if (satisfies(f, a)) return a;
    }
    return std::nullopt;
}

inline std::string literal_text(int literal) {
    return (literal < 0 ? "¬x" : "x") + std::to_string(std::abs(literal));
}

inline std::string clause_text(const Clause& c) {
    std::string text = "(";
    for (std::size_t i = 0; i < c.size(); i++) text += (i ? " ∨ " : "") + literal_text(c[i]);
    return text + ")";
}

inline std::string formula_text(const Formula& f) {
    std::string text;
    for (std::size_t i = 0; i < f.clauses.size(); i++) text += (i ? " ∧ " : "") + clause_text(f.clauses[i]);
    return text;
}

inline std::string assignment_text(const Assignment& a) {
    std::string text;
    for (std::size_t v = 1; v < a.size(); v++) {
        text += (v > 1 ? " " : "") + ("x" + std::to_string(v)) + "=" + (a[v] ? "V" : "F");
    }
    return text;
}

// Las ocho cláusulas posibles con tres variables: ninguna asignación las cumple todas.
inline Formula all_eight_clauses() {
    Formula f{3, {}};
    for (int mask = 0; mask < 8; mask++) {
        f.clauses.push_back({mask & 1 ? 1 : -1, mask & 2 ? 2 : -2, mask & 4 ? 3 : -3});
    }
    return f;
}