// La reducción de 3-SAT a conjunto independiente: un triángulo por cláusula y una arista entre cada
// par de literales opuestos. La fórmula se cumple si y solo si hay un conjunto independiente de tamaño k,
// con k igual al número de cláusulas.
#pragma once
#include <cstddef>
#include <vector>
#include "cnf.h"
#include "graph.h"

struct IndependentSetInstance {
    Graph graph;
    int k = 0;
    std::vector<int> literal;  // literal[nodo] es el literal que representa ese nodo
};

// Las dos banderas existen para ver qué pasa si falta cada clase de aristas.
inline IndependentSetInstance reduce_to_independent_set(const Formula& f, bool triangles = true, bool conflicts = true) {
    IndependentSetInstance out;
    out.k = static_cast<int>(f.clauses.size());
    for (const Clause& c : f.clauses) out.literal.insert(out.literal.end(), c.begin(), c.end());
    out.graph.assign(out.literal.size(), {});
    int base = 0;
    for (const Clause& c : f.clauses) {
        int size = static_cast<int>(c.size());
        for (int i = 0; triangles && i < size; i++) {
            for (int j = i + 1; j < size; j++) add_edge(out.graph, base + i, base + j);
        }
        base += size;
    }
    int nodes = static_cast<int>(out.literal.size());
    for (int u = 0; conflicts && u < nodes; u++) {
        for (int v = u + 1; v < nodes; v++) {
            if (out.literal[static_cast<std::size_t>(u)] == -out.literal[static_cast<std::size_t>(v)]) add_edge(out.graph, u, v);
        }
    }
    return out;
}

// De una asignación a un conjunto: el primer literal verdadero de cada cláusula.
inline std::vector<int> set_from_assignment(const Formula& f, const Assignment& a) {
    std::vector<int> nodes;
    int base = 0;
    for (const Clause& c : f.clauses) {
        for (std::size_t i = 0; i < c.size(); i++) {
            if (literal_true(a, c[i])) {
                nodes.push_back(base + static_cast<int>(i));
                break;
            }
        }
        base += static_cast<int>(c.size());
    }
    return nodes;
}

// De un conjunto a una asignación: lo elegido es verdadero. El resto de variables da igual: quedan en F.
inline Assignment assignment_from_set(const Formula& f, const IndependentSetInstance& instance, const std::vector<int>& nodes) {
    Assignment a(static_cast<std::size_t>(f.variables) + 1, false);
    for (int v : nodes) {
        int literal = instance.literal[static_cast<std::size_t>(v)];
        a[static_cast<std::size_t>(std::abs(literal))] = literal > 0;
    }
    return a;
}