Java SAT (Haltbarkeitsproblem) mit Regex

Hallo,
ich bin gerade dabei ein Programm zu schreiben, welches das Erfüllbarkeitsproblem löst (bzw. SAT = satisfiability problem). Hierzu darf die aussagenlogische Formal aus dem Alphabet: X,1,0,(,),V,&,- bestehen. Dabei steht das „V“ für Oder, das „&“ für UND und das „–„ für die Negation. Mit X,1,0 lassen sich somit auch alle Zahlen kodieren (z.B. die Zahl 1 = X01, 2= X02 usw.). Damit nur dieses Alphabet vorkommt, verwende ich das Pattern machting. Dies wird wie folgt geprüft:


Java:
public void suche(String eingabe) {
        
        if(Pattern.matches("[X10()V&-]+", eingabe) == true)
        {
            System.out.println("Eingabestring ist zulässig");
        }
        else
        {
            System.out.println("Eingabestring ist unzulässig");
        }


Nun habe ich einige Schwierigkeiten:
1)
Damit syntaktische Korrektheit garantiert wird, sollten die Konstellationen wie „ X1 V& X2“, „X1 VV X2“, „X1 && X2“ nicht zugelassen werden.
Frage: Gibt es eine Möglichkeit mit dem Pattern-Matching diese Konstellationen auszuschließen, sodass z.B. diese als „false“ angesehen werden und die Nachricht „Eingabestring ist unzulässig“ ausgegeben wird? Ich habe schon sehr viel im Internet dazu gesucht aber leider nichts gefunden.

2)
Nachdem ich die syntaktische Korrektheit erlangt habe, geht’s zum Auswerten. Kann mir da jemand vielleicht einen Tipp geben, wie ich am besten diese aussagenlogischen Ausdrücke auswerten kann? Auf dem Blattpapier würde ich hierzu eine Baumstruktur erstellen und mit der innersten Klammer anfangen. Wenn die Formel wie folgt aussieht :
(X10 V X01)-((X11 & X01) V X10))
3. 1. 2.
-- Dann würde ich zuerst 1. Auswerten, dann mit 2. Auswerten und anschließend das ganze mit 3. Auswerten.
Frage: Wie könnte ich das in Java umsetzen ? Hat da jemand ein Vorschlag für mich?

3)
Es gibt noch einen speziellen Fall, der ebenfalls direkt ausgeschlossen werden soll.
Wenn dieselbe Variable mit einem UND verknüpft wird, und eine davon negiert ist, dann soll ist dieser Bereich schon mal nicht erfüllbar. Dies sieht dann wie folgt aus:
(X1 & -X1) --> nicht erfüllbar.
Frage: Wie könnte ich dies mein Programm erkennen lassen? Es sollte hier also erkannt wird, dass dieselbe Variable (einmal z.B. X1 und einmal negiert X1) mit der Operation & verknüpft wurde?

Ich bedanke mich schon mal für die Tipps und Denkanstöße.
 
mMn auf jeden Fall nicht mit Regex. Ich würde da Fall eine Art Parser verwenden. Dieser kann dann auch die Gültigkeit prüfen.
 
Zuletzt bearbeitet:
Ich sehe zwei Möglichkeiten:
a) Einen bestehenden Parser verwenden, für den man dann eine Grammatik definiert (z.B. eine Backus-Naur-Form: https://de.wikipedia.org/wiki/Backus-Naur-Form).
Vorteil: Man muss keinen Parser schreiben
Nachteil: Man muss die Grammatik definieren und nach dem Parsen mittels der Grammatik das noch seine eigene Datenstruktur bringen
b) Einen eigenen Parser
Vorteil: Man kann es direkt in seine eigene Datenstruktur bringen
Nachteil: Man muss den Parser schreiben

Ich würde zu b) tendieren - aber das erst mal hinten anstellen.

Ich würde das Pferd von der anderen Seite aufzäumen. Erstmal deine Datenstrukturen definieren, mit denen du auswerten willst. Und sobald du die hast, kannst du dir dann überlegen, wie du die Daten parst. Aber dann weißt du wo du hin willst - und kannst auch besser bewerten, welcher Ansatz passt.
 
Ok vielen
Ich sehe zwei Möglichkeiten:
a) Einen bestehenden Parser verwenden, für den man dann eine Grammatik definiert (z.B. eine Backus-Naur-Form: https://de.wikipedia.org/wiki/Backus-Naur-Form).
Vorteil: Man muss keinen Parser schreiben
Nachteil: Man muss die Grammatik definieren und nach dem Parsen mittels der Grammatik das noch seine eigene Datenstruktur bringen
b) Einen eigenen Parser
Vorteil: Man kann es direkt in seine eigene Datenstruktur bringen
Nachteil: Man muss den Parser schreiben

Ich würde zu b) tendieren - aber das erst mal hinten anstellen.

Ich würde das Pferd von der anderen Seite aufzäumen. Erstmal deine Datenstrukturen definieren, mit denen du auswerten willst. Und sobald du die hast, kannst du dir dann überlegen, wie du die Daten parst. Aber dann weißt du wo du hin willst - und kannst auch besser bewerten, welcher Ansatz passt.
Ok vielen Dank schon mal für die Antwort. Wenn ich die Grammatik definiert habe, wie könnte ich dann weiter machen? Ich müsste ja irgendwie zuerst an die innerste Klammer kommen und diese berechnen? Hättest du dafür vielleicht auch einen Ansatz?
 
Frage: Gibt es eine Möglichkeit mit dem Pattern-Matching diese Konstellationen auszuschließen, sodass z.B. diese als „false“ angesehen werden
Nein, reguläre Ausdrücke sind prinzipiell nicht zum Arbeiten auf rekursiven Strukturen geeignet.

Ich habe mal gelesen, dass es in Pearl Erweiterungen dazu gibt, habe aber keine konkrete Ahnung.

In einem Java-Magazin vor langer Zeit (2002 oder 2003) gab es mal einen Artikel über das Verfahren "rekursiver Abstieg".

Nach diesem Prinzip habe ich meine Parser geschrieben.

Wahrscheinlich findest Du im Netz auch was darüber.
 
Passende Stellenanzeigen aus deiner Region:

Neue Themen

Oben