Algorithmische Strategien für anwendbare reelle Quantorenelimination

Abstract

Eines der bedeutendsten Verfahren zur reellen Quantorenelimination ist die Quantorenelimination mittels virtueller Substitution, die von Weispfenning 1988 eingeführt wurde. In der vorliegenden Arbeit werden zahlreiche algorithmische Strategien zur Optimierung dieses Verfahrens präsentiert. Optimierungsziele der Arbeit waren dabei die tatsächliche Laufzeit der Implementierung des Algorithmus sowie die Größe der Ausgabeformel. Zur Optimierung werden dabei die Simplifikation von Formeln erster Stufe, die Reduktion der Größe der Eliminationsmenge sowie das Condensing, ein Ersatz für die virtuelle Substitution, untersucht. Lokale Quantorenelimination berechnet Formeln, die nur in der Nähe eines gegebenen Punktes äquivalent zur Eingabeformel ist. Diese Einschränkung erlaubt es, das Verfahren weiter zu verbessern. Als Anwendung des Eliminationsverfahren diskutieren wir abschließend, wie man eine große Klasse von Schedulingproblemen mittels reeller Quantorenelimination lösen kann. In diesem Fall benutzen wir die spezielle Struktur der Eingabeformel und zusätzliche Informationen über das Schedulingproblem, um die Quantorenelimination mittels virtueller Substitution problemspezifisch zu optimieren.