#!/usr/bin/env python3

# Konfliktsuche.py
"""
Anhang Fehlerdiagnose: Den Konflikt finden, der INFEASIBLE verursacht.

Ein Deletion Filter (auch: IIS, Irreducible Infeasible Subset) isoliert aus
einem unloesbaren Modell eine kleinste widerspruechliche Teilmenge von
Bedingungen: Nimmt man aus ihr auch nur eine einzige Bedingung heraus, ist
der Rest wieder loesbar.

Das Programm zeigt sechs Dinge:
  1. Der Solver meldet INFEASIBLE - und sonst nichts.
  2. Die naive Suche ("jede Bedingung einmal weglassen") findet hier gar nichts.
  3. Der Deletion Filter findet einen Konflikt in n Solveraufrufen.
  4. Ein Konflikt ist selten einer: nach der Reparatur folgt der naechste.
  5. "Den" kleinsten Konflikt gibt es nicht - dieses Modell enthaelt neun.
  6. Welchen davon man zu sehen bekommt, steuert die Pruefreihenfolge.

Abgrenzung zu Infeasibility_Diagnose.py (Kapitel Praxisfallen): Dort geht es
um die Relaxation - das Modell soll trotz Widerspruch eine brauchbare Antwort
liefern. Hier geht es um die Diagnose - welche Bedingungen widersprechen sich
ueberhaupt. Beides zusammen ergibt den Umgang mit INFEASIBLE in Produktion.

Benoetigt: numpy, scipy
"""

from __future__ import annotations

import numpy as np
from scipy.optimize import linprog

PRODUKTE = ["Rahmen", "Gehaeuse", "Deckel", "Traeger", "Halter"]

# Jede Bedingung traegt einen sprechenden Namen - das ist keine Kosmetik,
# sondern die Voraussetzung dafuer, dass der Befund lesbar wird.
# (Name, Koeffizienten je Produkt, Richtung, rechte Seite)
BEDINGUNGEN: list[tuple[str, list[float], str, float]] = [
    ("Kapazitaet Montage",       [3, 2, 1, 4, 2],      "<=",   400),
    ("Kapazitaet Lackieren",     [2, 3, 0, 1, 0],      "<=",   150),
    ("Kapazitaet Pruefung",      [1, 1, 1, 1, 1],      "<=",   300),
    ("Liefervertrag Rahmen",     [1, 0, 0, 0, 0],      ">=",    40),
    ("Liefervertrag Gehaeuse",   [0, 1, 0, 0, 0],      ">=",    30),
    ("Liefervertrag Deckel",     [0, 0, 1, 0, 0],      ">=",    20),
    ("Liefervertrag Traeger",    [0, 0, 0, 1, 0],      ">=",    25),
    ("Marktgrenze Rahmen",       [1, 0, 0, 0, 0],      "<=",   120),
    ("Marktgrenze Gehaeuse",     [0, 1, 0, 0, 0],      "<=",    90),
    ("Marktgrenze Deckel",       [0, 0, 1, 0, 0],      "<=",   150),
    ("Marktgrenze Halter",       [0, 0, 0, 0, 1],      "<=",   200),
    ("Mindestumsatz",            [90, 70, 30, 60, 20], ">=", 12000),
    ("Sortimentsbreite",         [0, 0, 1, 1, 1],      ">=",   100),
    ("Lackierbudget Schicht 2",  [0, 1, 0, 1, 0],      "<=",    55),
]

# Welche Bedingungen koennte ein Planer im Ernstfall wirklich veraendern?
# Kapazitaeten lassen sich durch Sonderschichten dehnen, Liefervertraege und
# Marktgrenzen nicht.
VERHANDELBAR = {"Kapazitaet Montage", "Kapazitaet Lackieren",
                "Kapazitaet Pruefung", "Lackierbudget Schicht 2"}

aufrufe = 0          # zaehlt jeden Solveraufruf mit - der Preis des Verfahrens


def ist_loesbar(auswahl: list[int]) -> bool:
    """Gibt es einen Punkt, der ALLE Bedingungen aus 'auswahl' erfuellt?

    Es wird nur Zulaessigkeit geprueft, keine Zielfunktion optimiert: die
    Zielfunktion ist konstant null. INFEASIBLE haengt nie an der Zielfunktion.
    """
    global aufrufe
    aufrufe += 1
    matrix, rechte_seite = [], []
    for i in auswahl:
        _, koeffizienten, richtung, grenze = BEDINGUNGEN[i]
        zeile = np.array(koeffizienten, dtype=float)
        # linprog kennt nur "<=", also ">=" durch Negation umdrehen
        matrix.append(zeile if richtung == "<=" else -zeile)
        rechte_seite.append(grenze if richtung == "<=" else -grenze)
    ergebnis = linprog(np.zeros(len(PRODUKTE)),
                       A_ub=np.array(matrix), b_ub=np.array(rechte_seite),
                       bounds=(0, None), method="highs")
    return ergebnis.status == 0


def deletion_filter(auswahl: list[int]) -> list[int]:
    """Verkleinert eine unloesbare Menge zu einer kleinsten unloesbaren Menge.

    Der Kern des Verfahrens ist eine einzige Regel: Nimm eine Bedingung
    versuchsweise heraus. Bleibt der Rest unloesbar, wurde sie fuer den
    Widerspruch nicht gebraucht - sie darf endgueltig weg. Wird der Rest
    loesbar, war sie beteiligt und muss bleiben.

    Nach genau einem Durchlauf ueber alle Bedingungen ist das Ergebnis
    unreduzierbar: n Solveraufrufe statt 2^n Teilmengen.
    """
    rest = list(auswahl)
    for i in list(auswahl):
        probe = [j for j in rest if j != i]
        if not ist_loesbar(probe):
            rest = probe
    return rest


def namen(auswahl: list[int]) -> list[str]:
    return [BEDINGUNGEN[i][0] for i in auswahl]


def teil_1_der_befund(alle: list[int]) -> None:
    print("=" * 68)
    print("1. Was der Solver sagt")
    print("=" * 68)
    print(f"Modell: {len(PRODUKTE)} Variablen, {len(BEDINGUNGEN)} Bedingungen")
    status = "OPTIMAL" if ist_loesbar(alle) else "INFEASIBLE"
    print(f"Status: {status}")
    print("\nMehr ist es nicht. Der Solver nennt keine Ursache, weil es die eine")
    print("Ursache nicht gibt: Unloesbarkeit ist eine Eigenschaft von Mengen von")
    print("Bedingungen, nicht von einzelnen Bedingungen.")


def teil_2_die_naive_suche(alle: list[int]) -> None:
    print("\n" + "=" * 68)
    print("2. Die naheliegende Idee - und warum sie hier scheitert")
    print("=" * 68)
    print("Jede Bedingung einmal weglassen und schauen, ob es dann geht:\n")
    treffer = [i for i in alle if ist_loesbar([j for j in alle if j != i])]
    for i in alle:
        print(f"   ohne {BEDINGUNGEN[i][0]:<26} {'loesbar' if i in treffer else 'weiter unloesbar'}")
    print(f"\nGefundene Schuldige: {len(treffer)}")
    print("Keine einzelne Bedingung ist schuld. Genau das ist der Normalfall -")
    print("und der Grund, warum diese Suche in der Praxis so oft im Nichts endet.")


def teil_3_der_filter(alle: list[int]) -> list[int]:
    global aufrufe
    print("\n" + "=" * 68)
    print("3. Der Deletion Filter")
    print("=" * 68)
    vorher = aufrufe
    konflikt = deletion_filter(alle)
    kosten = aufrufe - vorher
    print(f"{kosten} Solveraufrufe -> Konflikt aus {len(konflikt)} von "
          f"{len(BEDINGUNGEN)} Bedingungen:\n")
    for name in namen(konflikt):
        print(f"   * {name}")
    print("\nProbe auf Unreduzierbarkeit - jede einzelne davon weglassen:")
    for i in konflikt:
        rest_loesbar = ist_loesbar([j for j in konflikt if j != i])
        print(f"   ohne {BEDINGUNGEN[i][0]:<26} {'loesbar' if rest_loesbar else 'UNLOESBAR - nicht minimal!'}")
    print(f"\nAufwand: {kosten} Aufrufe. Alle Teilmengen durchzuprobieren waeren "
          f"2^{len(BEDINGUNGEN)} = {2 ** len(BEDINGUNGEN):,} gewesen.".replace(",", "."))
    return konflikt


def teil_4_der_naechste_konflikt(alle: list[int], konflikt: list[int]) -> None:
    print("\n" + "=" * 68)
    print("4. Ein Konflikt ist selten einer")
    print("=" * 68)
    entfernt = konflikt[0]
    rest = [i for i in alle if i != entfernt]
    print(f"Angenommen, '{BEDINGUNGEN[entfernt][0]}' laesst sich verhandeln")
    print("und wird aus dem Modell genommen. Dann ist das Modell ...")
    if ist_loesbar(rest):
        print("... loesbar. Fertig.")
        return
    print("... immer noch unloesbar. Der Filter erneut:\n")
    zweiter = deletion_filter(rest)
    for name in namen(zweiter):
        print(f"   * {name}")
    gemeinsam = set(zweiter) & set(konflikt)
    print(f"\nUeberschneidung mit dem ersten Konflikt: {len(gemeinsam)} Bedingungen")
    print("Ein zweiter, unabhaengiger Widerspruch, den der erste verdeckt hat.")
    print("Deshalb ist die Konfliktsuche eine Schleife, kein einzelner Aufruf:")
    print("reparieren, neu suchen, bis das Modell loesbar ist.")


def teil_5_die_reihenfolge(alle: list[int]) -> None:
    print("\n" + "=" * 68)
    print("5. Es gibt nicht DEN Konflikt")
    print("=" * 68)
    print("Derselbe Filter, nur eine andere Pruefreihenfolge - 200-mal gewuerfelt:\n")
    zufall = np.random.default_rng(0)
    haeufigkeit: dict[tuple[int, ...], int] = {}
    for _ in range(200):
        ordnung = [int(i) for i in zufall.permutation(alle)]
        schluessel = tuple(sorted(deletion_filter(ordnung)))
        haeufigkeit[schluessel] = haeufigkeit.get(schluessel, 0) + 1
    for schluessel, anzahl in sorted(haeufigkeit.items(), key=lambda p: -p[1]):
        print(f"   {anzahl:3d}x  {len(schluessel)} Bedingungen: "
              f"{', '.join(namen(list(schluessel)))}")
    print(f"\n{len(haeufigkeit)} verschiedene minimale Konflikte in EINEM Modell.")
    print("Der Filter liefert *einen* kleinsten Konflikt, nicht *den* kleinsten -")
    print("den gibt es nicht. Alle oben sind gleichermassen korrekt.")


def teil_6_den_befund_steuern(alle: list[int]) -> None:
    print("\n" + "=" * 68)
    print("6. Den Befund brauchbar machen")
    print("=" * 68)
    print("Der Filter wirft heraus, was er zuerst in die Hand bekommt. Wer die")
    print("unveraenderlichen Bedingungen zuerst pruefen laesst, bekommt sie eher")
    print("aus dem Befund heraus - und sieht dafuer mehr Stellschrauben.\n")
    fest = [i for i in alle if BEDINGUNGEN[i][0] not in VERHANDELBAR]
    frei = [i for i in alle if BEDINGUNGEN[i][0] in VERHANDELBAR]
    for titel, ordnung in (("unveraenderliche zuerst", fest + frei),
                           ("veraenderliche zuerst  ", frei + fest)):
        konflikt = sorted(deletion_filter(ordnung))
        stellschrauben = [i for i in konflikt if BEDINGUNGEN[i][0] in VERHANDELBAR]
        print(f"   {titel} -> {len(konflikt)} Bedingungen, davon "
              f"{len(stellschrauben)} veraenderlich")
        print(f"      {', '.join(namen(konflikt))}")
    print("\nBeide Befunde sind wahr. Nur einer davon nennt dem Planer etwas,")
    print("das er tatsaechlich tun kann.")


if __name__ == "__main__":
    alle = list(range(len(BEDINGUNGEN)))
    teil_1_der_befund(alle)
    teil_2_die_naive_suche(alle)
    konflikt = teil_3_der_filter(alle)
    teil_4_der_naechste_konflikt(alle, konflikt)
    teil_5_die_reihenfolge(alle)
    teil_6_den_befund_steuern(alle)
    print("\n" + "=" * 68)
    print(f"Insgesamt {aufrufe} Solveraufrufe fuer die gesamte Diagnose.")
    print("=" * 68)