// La reducción de SAT (en CNF) a 3-SAT. La salida tiene exactamente tres literales por cláusula, de
// tres variables distintas. Es equisatisfactible con la entrada, no equivalente: agrega variables.
#pragma once
#include <algorithm>
#include <cstddef>
#include <cstdlib>
#include <vector>
#include "cnf.h"

// Quita literales repetidos. Devuelve false si la cláusula tiene x y ¬x, y entonces siempre se cumple.
inline bool clean_clause(const Clause& input, Clause& output) {
    output.clear();
    for (int literal : input) {
        if (std::find(output.begin(), output.end(), -literal) != output.end()) return false;
        if (std::find(output.begin(), output.end(), literal) == output.end()) output.push_back(literal);
    }
    return true;
}

inline Formula to_three_sat(const Formula& f) {
    Formula out{f.variables, {}};
    Clause c;
    for (const Clause& input : f.clauses) {
        if (!clean_clause(input, c)) continue;
        const std::size_t k = c.size();
        if (k == 0) {
            // La cláusula vacía nunca se cumple: las 8 cláusulas sobre tres variables nuevas tampoco.
            int y = out.variables + 1;
            out.variables += 3;
            for (int mask = 0; mask < 8; mask++) {
                out.clauses.push_back({mask & 1 ? y : -y, mask & 2 ? y + 1 : -(y + 1), mask & 4 ? y + 2 : -(y + 2)});
            }
        } else if (k == 1) {
            int y = ++out.variables;
            int z = ++out.variables;
            out.clauses.push_back({c[0], y, z});
            out.clauses.push_back({c[0], y, -z});
            out.clauses.push_back({c[0], -y, z});
            out.clauses.push_back({c[0], -y, -z});
        } else if (k == 2) {
            int y = ++out.variables;
            out.clauses.push_back({c[0], c[1], y});
            out.clauses.push_back({c[0], c[1], -y});
        } else if (k == 3) {
            out.clauses.push_back(c);
        } else {
            // Una cadena: yⱼ dice "el literal verdadero está más adelante".
            int y = ++out.variables;
            out.clauses.push_back({c[0], c[1], y});
            for (std::size_t i = 2; i + 2 < k; i++) {
                int next = ++out.variables;
                out.clauses.push_back({-y, c[i], next});
                y = next;
            }
            out.clauses.push_back({-y, c[k - 2], c[k - 1]});
        }
    }
    return out;
}

// La dirección "de ida" de la demostración: extiende una asignación de f a las variables nuevas. Recorre
// las cláusulas en el mismo orden que to_three_sat, así que asigna las mismas variables nuevas.
inline Assignment extend_assignment(const Formula& f, const Assignment& a, int total_variables) {
    Assignment out(static_cast<std::size_t>(total_variables) + 1, false);
    for (std::size_t v = 1; v < a.size(); v++) out[v] = a[v];
    std::size_t next = a.size();
    Clause c;
    for (const Clause& input : f.clauses) {
        if (!clean_clause(input, c)) continue;
        const std::size_t k = c.size();
        if (k == 0) {
            next += 3;
        } else if (k == 1) {
            next += 2;
        } else if (k == 2) {
            next += 1;
        } else if (k > 3) {
            // i es la posición de un literal verdadero, contando desde 1. yⱼ es verdadera si i ≥ j + 2.
            std::size_t i = 1;
            while (i <= k && !literal_true(a, c[i - 1])) i++;
            for (std::size_t j = 1; j + 3 <= k; j++) out[next++] = i >= j + 2;
        }
    }
    return out;
}