// Coloreo de grafos como CNF: una variable por cada (nodo, color).
#ifndef COLORING_H
#define COLORING_H

#include <vector>

#include "cnf.h"
#include "graphs.h"

inline int color_variable(int node, int color, int colors) { return node * colors + color + 1; }

// Cada nodo tiene al menos un color, y dos vecinos no comparten ninguno. "A lo sumo un color por nodo" es opcional.
inline Cnf encode_coloring(const Graph& g, int colors, bool at_most_one) {
    Cnf formula;
    formula.variables = g.n * colors;
    std::vector<int> vars(colors);
    for (int v = 0; v < g.n; v++) {
        for (int c = 0; c < colors; c++) vars[c] = color_variable(v, c, colors);
        add_at_least_one(formula, vars);
        if (at_most_one) add_at_most_one(formula, vars);
    }
    for (auto [u, v] : g.edges) {
        for (int c = 0; c < colors; c++) formula.add({-color_variable(u, c, colors), -color_variable(v, c, colors)});
    }
    return formula;
}

// Lee el primer color verdadero de cada nodo.
inline std::vector<int> decode_coloring(const Graph& g, int colors, const Assignment& value) {
    std::vector<int> color(g.n, -1);
    for (int v = 0; v < g.n; v++) {
        for (int c = colors - 1; c >= 0; c--) {
            if (value[color_variable(v, c, colors)]) color[v] = c;
        }
    }
    return color;
}

// Cuántos colores verdaderos tiene cada nodo.
inline std::vector<int> true_colors(const Graph& g, int colors, const Assignment& value) {
    std::vector<int> count(g.n, 0);
    for (int v = 0; v < g.n; v++) {
        for (int c = 0; c < colors; c++) count[v] += value[color_variable(v, c, colors)] ? 1 : 0;
    }
    return count;
}

#endif