Algorithmen für FD-Solver (Ansatz)

zum Lösen eines Constraint-Systems F: -- DPLL für SAT:

• Zustand (Knoten im Suchbaum) ist partielle Belegung b
• Def.: b₁≤b₂ falls b₁⊇b₂,

  (F, b) ist konsistent (erfüllbar): ∃b'≤b : b' $\models$ F

• Invariante:

  für jeden Knoten b mit Kindern b₁(, b₂) gilt: b_i≤b und

  ((F, b) konsistent $\iff$ b $\models$ F∨∃i : (F, b_i) konsistent)

grundsätzliches Vorgehen bei FD:

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

  ordnet jeder Variablen eine Teilmenge (domain) von U zu

• Inv.: für dom mit Kindern dom₁,… gilt: dom_i≤dom und

  ( (F, dom) kons. ⇔ (F, dom) gelöst ∨∃i : (F, dom_i) kons.).