41 

 

𝛱𝜀𝛿ί𝜊 𝛰𝜌𝜄𝜎𝜇𝜊ύ:  Έ𝜎𝜏𝜔 𝐷 = {1,2,3,4}   → {[[𝑥 ≥ 1]], [[𝑥 ≤ 4]]} 

(2.13)

 

𝛱𝜀𝜌𝜄𝜊𝜌𝜄𝜎𝜇ό𝜍:  𝐶1 = [[𝑥 ≤ 𝑧]] → [[𝑥 ≤ 𝑧 + 1]]  

 

 

(2.14)

 

𝛱𝜀𝜌𝜄𝜊𝜌𝜄𝜎𝜇ό𝜍:  𝐶2 = [[𝑥 = 𝑧]] → [[𝑥 ≤ 𝑧 ]] ∧ ¬[[𝑥 ≤ 𝑧 − 1 ]] 

(2.15)

 

Οι  ατομικοί  περιορισμοί  όπως  η  ανάθεση  τιμής,  οι  αλλαγές  πεδίων  ορισμού  ή  η  αφαίρεση 

τιμών από ένα πεδίο ορισμού είναι απλά κυριολεκτικά (literals) όπως στα SAT. 

Η  αναζήτηση  ελέγχεται  από  έναν  επιλυτή  FD.  Σε  κάθε  διάδοση  περιορισμού,  ο 

επιλυτής FD καταγράφει προτάσεις επεξήγησης και τις αποστέλλει στον εσωτερικό επιλυτή 

SAT  ενεργοποιώντας  τον  με  προτεραιότητα  εκτέλεσης.  Αφού  ενεργοποιηθεί,  δρα  σαν 

καθολικός μηχανισμός διάδοσης με την υψηλότερη προτεραιότητα διάδοσης. 

Όταν  εκτελείται  ένας  μηχανισμός  διάδοσης  του  επιλυτή  FD  για  να  τροποποιήσει  το 

πεδίο  ορισμού,  δημιουργεί  μία  πρόταση  επεξήγησης  (explanation  clause)  κατά  την  οποία 

εξηγεί το λόγο που έγιναν αλλαγές σε ατομικούς περιορισμούς. Για παράδειγμα, η έκφραση 

[𝑥 ≤ 2] ∧ [𝑥 ≥ 𝑦] σημαίνει πως [𝑦 ≤ 2] και δημιουργείται η πρόταση [𝑥 ≤ 2] → [𝑦 ≤ 2] ως 

δικαιολόγηση. Σε περίπτωση αποτυχίας, δηλαδή όταν ένα πεδίο ορισμού είναι κενό ύστερα 

από  αλλαγή,  ο  μηχανισμός  διάδοσης  πρέπει  να  εξηγήσει  και  την  αποτυχία.  Οι  προτάσεις 

επεξήγησης μπορούν να χρησιμοποιηθούν για τη δημιουργία nogoods τα οποία αξιοποιούνται 

εύκολα  από  τους  μηχανισμούς  διάδοσης  του  SAT.  Τα  nogoods  επιτρέπουν  την  παράλειψη 

ενός  μεγάλου  υποσυνόλου  του  χώρου  αναζήτησης  ενώ  παράλληλα  επιτρέπουν  τη  σωστή 

επιλογή του επιπέδου που θα γίνει η (μη-χρονολογική) υπαναχώρηση. Οποιαδήποτε αλλαγή 

πραγματοποιεί ένας μηχανισμός διάδοσης μπορεί διαδοχικά να προκαλέσει την ενεργοποίηση 

άλλου μηχανισμού, με αυτόν τον κύκλο να εκτελείται έως ότου να φτάσει σε ένα ορισμένο 

σημείο. 

 

Εικόνα 2.14: Αρχιτεκτονική του LCG.