Algorithmen für FD-Solver

DPLL für SAT:

• Zustand (Knoten im Suchbaum) ist partielle Belegung
• Schritte (Kanten): Decide, Propagate, Conflict, Backtrack

grundsätzliches Vorgehen bei FD:

• Zustand ist Bereichs-Abbildung: dom : V→2^U

• Decide: wähle d∈dom(v), Kind-Knoten dom'(v) = {d}
• Backtrack: wähle ein anderes d'∈dom(v)
• Conflict: dom fehlgeschlagen
• Propagate: verkleinere die Domains von Variablen

  (schließe Werte aus, die zu Inkonsistenzen führen)

  dafür gibt es (im Unterschied zu DPLL) viele Varianten