FD und SAT

• für alle konsistenz-basierten Methoden gilt

  wenn man nichts mehr propagieren kann, muß man entscheiden

• dabei wählt man einen aus evtl. sehr vielen Werten, d.h. man muß später oft zurückkehren (backtrack)
• man könnte sich zunächst nur für die linke oder rechte Hälfte eines Intervalls entscheiden (dann nur ein Backtrack)
• das entspricht einer Binärdarstellung

  dann kann man gleich ein aussagenlogisches Constraintsystem benutzen: der Löser kann dann Klauseln lernen usw.