background image

40 

 

εξετάζοντας  μικρά  κομμάτια  της  έκφρασης  CNF  και  αναθέτοντας  μια  βαθμολογία  σε  κάθε 

κυριολεκτικό l

 και στο συμπλήρωμά του ¬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)

 

Παράλληλα με τις μεταβλητές και για να μη γίνονται αχρείαστες αναθέσεις κωδικοποιούνται 

τα πεδία ορισμού και οι περιορισμοί σε προτάσεις με ανάλογες μετατροπές όπως: