65 

 

3.7.2 Εύρεση Λύσεων με CP-SAT 

 

Αμέσως μετά τη μοντελοποίηση του προβλήματος, το CP-SAT ενεργοποιείται για την 

εύρεση των συνεπών και πλήρων αναθέσεων για τα μπλοκ άκρης. Το μοντέλο κωδικοποιείται 

(με  χρονική  πολυπλοκότητα  Ο(n

2

))  από  το  LCG  για  να  μπορεί  να  επιλυθεί  ως  SAT  (Ο(2

n

)) 

ενώ παράλληλα να μπορεί να γίνει προεπεξεργασία του.  Με αυτό τον τρόπο μειώνονται τα 

πεδία  ορισμού  και  απλοποιούνται  οι  περιορισμοί  που  θα  κληθούν  να  επιβάλλουν  οι 

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

περιορισμοί  που  μοιράζονται  μεταβλητές.  Με  τη  χρήση  του  μηχανισμού  VSIDS, 

εξερευνούνται  πρώτα  τα  κυριολεκτικά  με  τις  περισσότερες  εμφανίσεις  στις  πρόσφατα 

εξεταζόμενες  προτάσεις.  Όπως  στην  περίπτωση  του  𝑋

1

  που  εμφανίζεται  σε  τρείς 

προτάσεις/περιορισμούς  στο  παράδειγμα  της  Εικόνας  3.17,  οι  αναθέσεις  κυριολεκτικών  με 

μεγάλη βαθμολογία συνήθως έχουν σημαντικό αντίκτυπο οπότε πρέπει να εξεταστούν νωρίς 

για αποφυγή συγκρούσεων. 

 

Το CP-SAT δημιουργεί το εσωτερικό μοντέλο για τον επιλυτή SAT ενώ ταυτόχρονα 

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

συνδυασμός  αναθέσεων.  Με  την  εύρεση  αναθέσεων  που  ικανοποιούν  όλους  τους 

περιορισμούς  σχηματίζονται  οι  πλήρεις  και  συνεπείς  λύσεις  οι  οποίες  αξιοποιούν  ένα 

συγκεκριμένο αριθμό ναρκών [Εικόνα 3.18]. Οι αναθέσεις μίας λύσης αφορούν αποκλειστικά 

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

ταμπλό που περιλαμβάνουν τις αναθέσεις της όπως περιγράφει η εξίσωση 3.9. 

𝛴𝜐𝜈𝛿𝜐𝛼𝜎𝜇𝜊ί 𝐶(𝑛, 𝑟) =  

𝑛!

(𝑟!(𝑛−𝑟)!)

, {

𝑛 = 𝜅𝜆𝜀𝜄𝜎𝜏ά 𝜇𝜋𝜆𝜊𝜅𝜍 − 𝜇𝜋𝜆𝜊𝜅 ά𝜅𝜌𝜂𝜍 ≥ 0 

𝑟 = 𝜅𝛼𝜃𝜊𝜆𝜄𝜅έ𝜍 𝜈ά𝜌𝜅𝜀𝜍 − 𝜈ά𝜌𝜅𝜀𝜍 𝜆ύ𝜎𝜂𝜍 ≥ 0

, 𝑛 > 𝑟 

(3.9)

 

 

Για  λόγους  σαφήνειας  αυτοί  θα  αποκαλούνται  «τοπικοί  συνδυασμοί».  Καθώς  οι 

υπολογισμοί μπορεί να αφορούν αριθμούς με εκατοντάδες ψηφία είναι δαπανηροί από άποψη 

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

παρτίδας  για  την  κλίμακα  δυσκολίας  «Expert»  είναι  𝐶(480,99) = 5.6 × 10

104

.    Το  κάθε 

ζεύγος  n  και  r  αποθηκεύεται  σε  μία  λίστα  μαζί  με  το  αποτέλεσμά  του  ώστε  να  μπορεί  να 

επαναχρησιμοποιηθεί και να εξοικονομηθούν πόροι. Οι τοπικοί συνδυασμοί προστίθενται σε 

κάθε μπλοκ στο οποίο είχε ανατεθεί νάρκη κατά την λύση. Παράλληλα, προστίθενται στους 

«καθολικούς  συνδυασμούς»  οι  οποίοι  συμπεριλαμβάνουν  τους  τοπικούς  συνδυασμούς  από 

κάθε  πιθανή  λύση  που  επέστρεψε  το  CP-SAT. Η  πιθανότητα  ένα  μπλοκ  άκρης  να  περιέχει 

νάρκη υπολογίζεται από την παρακάτω εξίσωση 3.10: