39 

 

πεδία ορισμού μορφής Boolean και περιορισμούς ως λογικές πράξεις. Το SAT ήταν το πρώτο 

NP-Complete  πρόβλημα  που  διατυπώθηκε  από  τον  Stephen  Cook  το  1971  [62].  Με 

κατάλληλη κωδικοποίηση ενός CSP μπορεί να επιλυθεί ως SAT. 

Κατά  τα  SAT  προσδιορίζεται  εάν  υπάρχει  ανάθεση  των  μεταβλητών  Χ

i

  ενός 

προβλήματος  αποκλειστικά  με  Boolean  τιμές  (𝐷

𝑖

= {𝑡𝑟𝑢𝑒, 𝑓𝑎𝑙𝑠𝑒})  η  οποία  να  επαληθεύει 

πάντα την έκφραση που ορίζει το πρόβλημα. Ως κυριολεκτικό l

i

 (literal) ορίζεται η ανάθεση 

σταθερής τιμής μίας μεταβλητής X

i

 ή το συμπλήρωμά της ως ¬l

i

. Μία πρόταση 𝐶 αποτελείται 

από  τη  διάζευξη  κυριολεκτικών  𝑙

1

∨   𝑙

2

  ∨   … ∨   𝑙

𝑛

  ενώ  ένας  τύπος  Συζευκτικής  Κανονικής 

Μορφής  (CNF)  από  τη  σύζευξη  προτάσεων 

𝐶

1

∧

  𝐶

2

 

∧

  … 

∧

  𝐶

𝑛

. 

Ένας  τύπος  CNF 

ικανοποιείται όταν υπάρχει η ανάθεση κυριολεκτικών l που να τηρεί κάθε πρόταση 𝐶. Κάθε 

έκφραση Boolean μπορεί να διατυπωθεί ως CNF για τη μείωση του χώρου αναζήτησης [68]. 

Οι σύγχρονοι επιλυτές SAT [68] βασίζονται στη χρήση δυαδικών μεταβλητών (με τα 

αντίστοιχα  κυριολεκτικά)  και  στους  τύπους  CNF.  Κατά  την  αναζήτηση  λύσης,  δομείται 

σταδιακά  μία  μερική  ανάθεση  έως  τη  συμπλήρωση  μίας  πλήρης  ανάθεσης.  Σε  κάθε  βήμα 

πρέπει  να  τηρείται  η  συνέπεια  ως  προς  κάθε  πρόταση  του  τύπου  CNF.  Οι  μηχανισμοί 

διάδοσης (και οι συνδυασμοί τους) είναι υπεύθυνοι για την τήρηση της συνέπειας αλλά και 

για  την  απλοποίηση  του  τύπου  όπου  είναι  εφικτό.  Έχουν  μηχανισμό  που  ανιχνεύει 

συγκρούσεις (δηλαδή αναθέσεις όπου δεν τηρείται η συνέπεια), ώστε να αναλυθούν και να 

εφαρμόσουν  αλγόριθμο  backjumping  υπαναχωρώντας  ένα  βήμα  πριν  την  επιλογή  της 

ανάθεσης  που  επέφερε  τη  σύγκρουση.  Σε  σύνθετα  προβλήματα,  οι  συγκρούσεις  είναι 

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

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

Δεν  υπάρχει  γνωστός  αλγόριθμος  ο  οποίος  να  λύνει  κάθε  SAT  αποδοτικά  και  το 

ερώτημα του αν υπάρχει αλγόριθμος πολυωνυμικού χρόνου που να τα επιλύει είναι ανάλογο 

του προβλήματος P=NP που αναφέρθηκε κατά την εισαγωγή του κεφαλαίου. Ωστόσο, έχουν 

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

χιλιάδες μεταβλητές και εκατομμύρια προτάσεις. 

 

2.6 Variable-State Independent Decaying Sum  

 

Ένας ευριστικός αλγόριθμος που μπορεί να εφαρμοστεί στην αναζήτηση ενός επιλυτή 

SAT είναι ο Variable-State Independent Decaying Sum (VSIDS) [69].  Ο αλγόριθμος ξεκινά