SAT Calculator – SAT Solver και CNF Editor
Το SAT Calculator είναι ένας ανοιχτού κώδικα επεξεργαστής SAT φορμουλών και ντετερμινιστικός SAT solver, σχεδιασμένος για τη μελέτη προβλημάτων Boolean satisfiability στο πλαίσιο της θεωρίας πολυπλοκότητας και της προτασιακής λογικής. Η εφαρμογή επιτρέπει στους χρήστες να δημιουργούν, να επεξεργάζονται και να αναλύουν SAT φόρμουλες σε συζευκτική κανονική μορφή (CNF) μέσω ενός διαδραστικού γραφικού περιβάλλοντος.
Ο επεξεργαστής υποστηρίζει τη δημιουργία και τροποποίηση μεταβλητών, literals και clauses, ενώ παράλληλα παρέχει μια σαφή οπτική αναπαράσταση της δομής της φόρμουλας. Οι χρήστες μπορούν να ορίζουν χειροκίνητα τιμές στις μεταβλητές, ώστε να παρατηρούν πώς διαφορετικές αποτιμήσεις επηρεάζουν τη συνολική φόρμουλα και να διαπιστώνουν αν αυτή αξιολογείται ως αληθής ή ψευδής.
Ο ενσωματωμένος ντετερμινιστικός SAT solver υπολογίζει όλες τις δυνατές αποτιμήσεις των μεταβλητών και εντοπίζει εκείνες που ικανοποιούν τη φόρμουλα. Έτσι οι χρήστες μπορούν να μελετούν τον χώρο λύσεων και να κατανοούν καλύτερα τη συμπεριφορά των SAT προβλημάτων.
Εκτός από την επίλυση φορμουλών, η εφαρμογή παρέχει εργαλεία λογικής ανάλυσης, όπως την εφαρμογή της μεθόδου resolution σε επιλεγμένα clauses. Με αυτόν τον τρόπο είναι δυνατό να γίνονται πειράματα με κανόνες resolution και να παρατηρείται πώς προκύπτουν νέα clauses κατά τη διαδικασία συλλογισμού.
Το SAT Calculator παρέχει επίσης στατιστικές πληροφορίες για μεταβλητές και clauses, βοηθώντας τους χρήστες να αναλύουν τη δομή και την πολυπλοκότητα της φόρμουλας. Οι φόρμουλες μπορούν να γραφτούν χειροκίνητα, να επικολληθούν από εξωτερικές πηγές ή να φορτωθούν από έτοιμα παραδείγματα που είναι διαθέσιμα στο διαδίκτυο.
Η εφαρμογή εκτελείται σε Windows και έχει υλοποιηθεί με χρήση WPF, C# και .NET Framework 4.7.2.
Μπορείτε να την κατεβάσετε από SAT Calculator για Windows ή να κατεβάσετε τον πηγαίο κώδικα του SAT Calculator στο GitHub github.com/kritikov/SATCalculator.
