Ich habe eine kleine App geschrieben, die Ausdrücke in abstrakte Syntaxbäume übersetzt. Im Moment verwende ich eine Reihe von Heuristiken gegen den Ausdruck, um zu entscheiden, wie man die Abfrage am besten auswertet. Leider gibt es Beispiele, die den Abfrageplan extrem schlecht machen.
Ich habe einen Weg gefunden, um glaubwürdiger zu machen, wie Abfragen bewertet werden sollen, aber ich muss meinen Ausdruck zuerst in CNF oder DNF setzen, um nachweisbar korrekte Antworten zu erhalten. Ich weiß, dass dies potenziell exponentielle Zeit und Raum ergeben könnte, aber für typische Abfragen, die meine Benutzer ausführen, ist dies kein Problem.
Die Umwandlung in CNF oder DNF mache ich immer von Hand, um komplizierte Ausdrücke zu vereinfachen. (Nun, vielleicht nicht die ganze Zeit, aber ich weiß, wie das gemacht wird, zB mit Demorgans Gesetzen, Verteilungsgesetzen, etc.). Ich bin mir jedoch nicht sicher, wie ich anfangen soll, das in eine Methode zu übersetzen, die ist als ein Algorithmus implementierbar. Ich habe mir Artikel über die Optimierung von Abfragen angeschaut, und einige beginnen mit "Nun, zuerst legen wir Dinge in CNF" oder "Zuerst legen wir Dinge in DNF", und sie scheinen nie ihre Methode dafür zu erklären.
Wo soll ich anfangen?
Der naive Vanille-Algorithmus für quantenfreie Formeln lautet:
Es ist mir unklar, ob Ihre Formeln quantifiziert sind. Aber selbst wenn sie es nicht sind, scheint es das Ende der Wikipedia-Artikel auf konjunktiven Normalform zu sein, und es ist - ungefähr äquivalent in der automatisierten Theormuster-Welt - klausale Normalform alter ego umreißt einen verwendbaren Algorithmus (und zeigt auf Referenzen, wenn Sie diese Transformation etwas schlauer machen wollen). Wenn du mehr brauchst, erzähle uns bitte, wo du auf Schwierigkeiten stößt.
Schau dir Ссылка an Beispiel:
%Vor%Ausgabe ist:
%Vor%AKTUALISIEREN : Jetzt bevorzuge ich dieses Logikpaket :
%Vor%Ich bin auf diese Seite gestoßen: Wie man eine Formel in CNF umwandelt . Es zeigt den Algorithmus zum Konvertieren eines booleschen Ausdrucks in CNF in Pseudocode. Hat mir geholfen, mit diesem Thema zu beginnen.
Tags und Links algorithm query-optimization boolean-expression