// Fórmulas en CNF. Las variables van de 1 a variables, y un literal negativo es la variable negada,
// igual que en DIMACS.
#ifndef CNF_H
#define CNF_H

#include <cstdlib>
#include <ostream>
#include <sstream>
#include <string>
#include <vector>

using Clause = std::vector<int>;

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

    void add(Clause clause) { clauses.push_back(std::move(clause)); }

    std::string to_dimacs() const {
        std::ostringstream out;
        out << "p cnf " << variables << ' ' << clauses.size() << '\n';
        for (const Clause& clause : clauses) {
            for (int literal : clause) out << literal << ' ';
            out << "0\n";
        }
        return out.str();
    }
};

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

inline bool literal_true(int literal, const Assignment& value) {
    return literal > 0 ? value[literal] : !value[-literal];
}

// El verificador de SAT: el certificado es la asignación, y se mira cada literal una vez.
inline bool satisfies(const Cnf& formula, const Assignment& value) {
    for (const Clause& clause : formula.clauses) {
        bool any = false;
        for (int literal : clause) any = any || literal_true(literal, value);
        if (!any) return false;
    }
    return true;
}

// Reglas sobre una lista de variables.
inline void add_at_least_one(Cnf& formula, const std::vector<int>& vars) { formula.add(vars); }

inline void add_at_most_one(Cnf& formula, const std::vector<int>& vars) {
    for (std::size_t i = 0; i < vars.size(); i++) {
        for (std::size_t j = i + 1; j < vars.size(); j++) formula.add({-vars[i], -vars[j]});
    }
}

inline void add_exactly_one(Cnf& formula, const std::vector<int>& vars) {
    add_at_least_one(formula, vars);
    add_at_most_one(formula, vars);
}

// Fuerza bruta: las 2^variables asignaciones. Llama a visit con cada una que satisface.
template <typename Visit>
long long for_each_model(const Cnf& formula, Visit visit) {
    long long models = 0;
    const long long total = 1LL << formula.variables;
    Assignment value(formula.variables + 1, false);
    for (long long mask = 0; mask < total; mask++) {
        for (int v = 1; v <= formula.variables; v++) value[v] = ((mask >> (v - 1)) & 1) != 0;
        if (satisfies(formula, value)) {
            models++;
            visit(value);
        }
    }
    return models;
}

inline long long count_models(const Cnf& formula) {
    return for_each_model(formula, [](const Assignment&) {});
}

// DPLL: propagar cláusulas unitarias y, si no hay ninguna, probar una variable con los dos valores.
// state[v]: 0 sin asignar, 1 verdadera, −1 falsa. Si se pasa trace, anota lo que va pasando.
class Dpll {
public:
    explicit Dpll(const Cnf& formula, std::ostream* trace = nullptr)
        : formula_(formula), trace_(trace), state_(formula.variables + 1, 0) {}

    bool solve() { return search(0); }

    bool value(int v) const { return state_[v] == 1; }
    long long decisions() const { return decisions_; }

private:
    const Cnf& formula_;
    std::ostream* trace_;
    std::vector<int> state_;
    long long decisions_ = 0;

    void note(int depth, const std::string& text) {
        if (trace_ != nullptr) *trace_ << std::string(2 * static_cast<std::size_t>(depth), ' ') << text << '\n';
    }

    // Devuelve false si alguna cláusula queda con todos sus literales falsos.
    bool propagate(int depth, std::vector<int>& assigned) {
        bool changed = true;
        while (changed) {
            changed = false;
            for (const Clause& clause : formula_.clauses) {
                int free_literal = 0, free_count = 0;
                bool is_true = false;
                for (int literal : clause) {
                    int s = state_[std::abs(literal)];
                    if (s == 0) {
                        free_literal = literal;
                        free_count++;
                    } else if ((s == 1) == (literal > 0)) {
                        is_true = true;
                    }
                }
                if (is_true) continue;
                if (free_count == 0) {
                    note(depth, "conflicto");
                    return false;
                }
                if (free_count == 1) {
                    state_[std::abs(free_literal)] = free_literal > 0 ? 1 : -1;
                    assigned.push_back(std::abs(free_literal));
                    note(depth, "unitaria: " + std::to_string(free_literal));
                    changed = true;
                }
            }
        }
        return true;
    }

    bool search(int depth) {
        std::vector<int> assigned;
        bool ok = propagate(depth, assigned);
        if (ok) {
            int v = 1;
            while (v <= formula_.variables && state_[v] != 0) v++;
            if (v > formula_.variables) return true;
            for (int s : {1, -1}) {
                decisions_++;
                note(depth, "decisión: " + std::to_string(s * v));
                state_[v] = s;
                if (search(depth + 1)) return true;
                state_[v] = 0;
            }
        }
        for (int v : assigned) state_[v] = 0;
        return false;
    }
};

#endif