40
εξετάζοντας μικρά κομμάτια της έκφρασης CNF και αναθέτοντας μια βαθμολογία σε κάθε
κυριολεκτικό l
i
και στο συμπλήρωμά του ¬l
i
. Η βαθμολογία είναι ανάλογη με τον αριθμό των
προτάσεων 𝐶 που χρησιμοποιούν την εκάστοτε μεταβλητή. Περιοδικά κατά την εκτέλεση και
αναζήτηση περισσότερων κομματιών της έκφρασης, ο VSIDS διαιρεί όλες τις βαθμολογίες
με μία σταθερά. Αυτό μεταφράζεται σε μείωση της επιρροής της παρουσίας κάποιας
μεταβλητής σε προτάσεις που έχουν εξεταστεί νωρίτερα και σε ενδυνάμωση των
βαθμολογιών με παρουσία σε πιο πρόσφατες προτάσεις. Ο VSIDS διαλέγει πάντα το
κυριολεκτικό της μεταβλητής που έχει τη μεγαλύτερη βαθμολογία για να αποφασίσει που θα
συνεχίσει την αναζήτηση.
Με οδηγό τις βαθμολογίες, το VSIDS μπορεί να εγγυηθεί πως κάθε ανάθεση τιμής σε
μεταβλητή ικανοποιεί το μεγαλύτερο αριθμό των πρόσφατων προτάσεων της έκφρασης CNF.
Δεδομένου ότι οι βαθμολογίες δεν επηρεάζονται από τις αναθέσεις, η υπαναχώρηση
(backtracking) του επιλυτή σε περίπτωση ασυνέπειας είναι ακόμα πιο εύκολη.
2.7 Lazy Clause Generation
Το LCG είναι μια υβριδική τεχνική που ενισχύει έναν επιλυτή SAT με τεχνικές
γραμμικού προγραμματισμού [Εικόνα 2.14] [70]–[72]. Συνδυάζει τα πλεονεκτήματα του
προγραμματισμού περιορισμών πεπερασμένου πεδίου ορισμού (Finite Domain Propagation)
με αυτά των επιλυτών SAT. Συγκεκριμένα, εκμεταλλεύεται τα μοντέλα υψηλού επιπέδου των
FD καθώς και την αποδοτική αυτόνομη αναζήτηση των SAT με τη χρήση του VSIDS και
nogoods (στοιχεία που καταγράφουν το λόγο κάποιας αποτυχίας). Ο επιλυτής LCG
κωδικοποιεί τις ακέραιες μεταβλητές του προβλήματος CSP σε μεταβλητές τύπου Boolean
και κάθε αλλαγή σε αυτές αντικατοπτρίζεται στα πεδία ορισμού τους. Θεωρητικά, αυτό
σημαίνει πως το CSP μπορεί να λυθεί όπως τα SAT με τα ανάλογα υπολογιστικά
προτερήματα.
Έστω ακέραιος x με αρχικό πεδίο ορισμού 𝑎
0
… 𝑎
𝑛
ισχύει:
𝛪𝜎ό𝜏𝜂𝜏𝛼: [[𝑥 = 𝑦]], 𝑎
0
≤ 𝑦 ≤ 𝑎
𝑛
(2.11)
𝛢𝜈𝜄𝜎ό𝜏𝜂𝜏𝛼: [[𝑥 ≤ 𝑧]], 𝑎
0
≤ 𝑧 < 𝑎
𝑛
− 1
(2.12)
Παράλληλα με τις μεταβλητές και για να μη γίνονται αχρείαστες αναθέσεις κωδικοποιούνται
τα πεδία ορισμού και οι περιορισμοί σε προτάσεις με ανάλογες μετατροπές όπως: