Query-Normalisierung/Vergleich?

[dawit]

Hallo,

ich schreibe gerade eine kleine Bibliothek zur Datenabfrage und stehe jetzt vor dem Problem, zwei Queries miteinander vergleichen zu müssen. Ein Query ist lediglich ein Ausdruck bestehend aus Variablen, booleschen Operatoren (nur and, or und not) und Vergeichsoperatoren. Ich möchte jetzt herausfinden, ob zwei Queries das gleiche Ergebnis liefern, und wenn nicht, ob der eine Query strikter als der andere ist (und dessen Ergebnis somit eine Untermenge des anderen Queries ist).
Mir fehlt jetzt irgendwie ein Ansatz. Klar ist, dass die booleschen Ausdrücke normalisiert werden müssen (vielleicht kanonische KNF/DNF? Oder (was ich gerade gefunden habe), https://en.wikipedia.org/wiki/Binary_decision_diagram?). Und dann muss ich herausfinden, ob die Constraints auf die Variablen (z.B. price < 10) beider Queries gleich sind oder ein Query strikter ist (braucht es dafür schon so was wie einen Theorem Prover? Oder geht das einfacher?).
Ist das ganze überhaupt einigermaßen Effizient lösbar?

Ich weiß, mir fehlen hier die formalen Grundlagen. Ich würde das gerne ändern, weiß aber nicht genau, worin ich mich vertiefen sollte.
Viele Grüße
David

[RustySpoon]

Du bist schon auf dem richtigen Dampfer. Prinzipiell kannst du dein Problem auf das Erfüllbarkeitsproblem der Aussagenlogik reduzieren und dann einen einen SAT-Solver darauf loslassen. Bisschen knifflig ist das Handling der Vergleiche, lässt sich aber relativ einfach lösen indem du die Variablen groundest. Alternativ lässt sich das auch sehr elegant via Antwortmengenprogrammierung lösen, was aber ungleich komplexer ist, wenn du nicht so fit im Thema bist.

Ich geb dir mal noch kurz einen Denkanstoß. Angenommen du möchtest prüfen ob zwei Queries Q1 und Q2 äquivalent sind. Dann konvertierst du diese in aussagenlogische Formeln F1 und F2 und untersuchst ob F3 = F1 <=> F2 gilt, sprich: unter allen Interpretationen (= Belegung aller aussagenlogischer Variablen in der Formel) wahr ist. Gilt F3 nicht, so kannst du dir die Modellmengen M1 und M2 von F1 und F2 anschauen und vergleichen. Ein Modell ist eine "wahre" Interpretation einer Formel. Ist M1 nun beispielsweise eine echte Untermenge von M2, so ist Q1 strikter als Q2.

Ich hoffe das hilft dir erstmal auf die Sprünge. Versuch mal dich da reinzufiddeln, so super komplex ist das eigentlich alles nicht. Ich bin leider etwas kurz angebunden, kann dir das aber später gerne nochmal detaillierter erklären. :D

[dawit]

Danke schon mal für die Antwort, werde mir das jetzt erst mal durchlesen! Und für detailliertere Erklärungen bin ich natürlich auch immer offen :)

EDIT:
Hab gleich ein paar Fragen:

1. Wie genau grounde ich Variablen? Ich kann sie ja nicht mit festen Werten ersetzen.
2. So, wie ich SAT-Solver verstanden habe, geben sie, wenn überhaupt, eine Lösung zurück. Um zu prüfen, ob Q1 strikter ist als Q2, bräuchte ich aber die kompletten Modellmengen von F1 und F2, oder?