Java SAT (Erfüllbarkeitsproblem) mit Regex

slitec

Mitglied
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= X10 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.
 
Zuletzt bearbeitet:
Hab zwar keinen blassen Schimmer von SAT, dafür umso mehr von RegEx..

Also zu 2)
Du kannst mit dem Pattern \(([^\(\)]+)\) eine Schleife durchgehen. Die Werte jeweils berechnen und einfügen. (Regex101 - online regex editor and debugger)
Pseudo-Code:
Code:
myString = '(X10 V X01)-((X11 & X01) V X10))';
myPattern = '\(([^\(\)]+)\)'
rx = new RegEx(myPattern);
//Nicht global!
do while rx.test(myString){
    formula = reg.exexute(myString0).submathces(0);        //Formel auslesen
    result = eval(formula);
    myString = rx.replace(myString, result);
}

Findet in der Reihenfolge (Ich ersetze das Resultat als A, B, C etc.
(X10 V X01)-((X11 & X01) V X10))
A-((X11 & X01) V X10))
A-(B V X10)
A-C



3) Herausfinden dass es da ist ist einfacher. Wenn ja, dann geh aus deinem Code raus
(X\d)\s+&\s+-\1
Mit der Klammer kannst du den Wert nehmen. Mit \1 wird derselbe Wert wieder genommen
https://regex101.com/r/xfdU4I/1
 
Zuletzt bearbeitet:
Hi vielen Dank schon mal. Dann müsste ich aber ja vorher wissen wie viel Klammern der Eingabestring besitzt? Kann ich die Anzahl der Klammern irgendwie automatisch bestimmen? Das
"myPattern" automatisch bestimmt wird ? Weil der Eingabestring ist nicht immer der selbe, kann also auch mal z.B. (X1VX01) vorkommen.
 
Nö, die Anzahl ist mit dieser Version beliebig. AUch der Inhalt ist da noch nicht wichtig, da nur auf Klammern geprüft wird

Ich habe mal schnell ein Test in PHP geschrieben
PHP:
parse('(X10 V X01)-((X11 & X01) V X10)');
parse('((X1VX01) V (X10 V X01))-((X11 & X01) V X10)');

function parse($myString){
    echo "<p>Orig:    {$myString}<p>";
    $myPattern = '/\(([^\(\)]+)\)/';
    $i = 0;
    echo '<table><tr><th>Step</th><th>Formula</th><th>new String</th></tr>';
    while(preg_match($myPattern, $myString, $matches)) {
        
        $formula = $matches[1];
        $result = "#".++$i;  //evaluate $formula;
        $myString = preg_replace($myPattern, $result, $myString, 1);
        echo "<tr><td>#{$i}</td><td>{$formula}</td><td>{$myString}</td></tr>";
    }
    echo '</table>';
}
Ausgabe:
2019-11-29_110721.jpg
 
Nö, die Anzahl ist mit dieser Version beliebig. AUch der Inhalt ist da noch nicht wichtig, da nur auf Klammern geprüft wird

Ich habe mal schnell ein Test in PHP geschrieben
PHP:
parse('(X10 V X01)-((X11 & X01) V X10)');
parse('((X1VX01) V (X10 V X01))-((X11 & X01) V X10)');

function parse($myString){
    echo "<p>Orig:    {$myString}<p>";
    $myPattern = '/\(([^\(\)]+)\)/';
    $i = 0;
    echo '<table><tr><th>Step</th><th>Formula</th><th>new String</th></tr>';
    while(preg_match($myPattern, $myString, $matches)) {
     
        $formula = $matches[1];
        $result = "#".++$i;  //evaluate $formula;
        $myString = preg_replace($myPattern, $result, $myString, 1);
        echo "<tr><td>#{$i}</td><td>{$formula}</td><td>{$myString}</td></tr>";
    }
    echo '</table>';
}
Ausgabe:
Anhang anzeigen 66185


Vielen vielen Dank erst mal für diese Antwort. Dies sieht schon mal sehr gut aus. Leider wird bei dem Erfüllbarkeitsproblem nicht diese Formel berechnet, sondern es wird für jedes X eine 0 oder eine 1 eingesetzt. So wird z.B. (X1 V X2) wie folgt geprüft:



X1X2(X1 V X2)
101
011
000
111



Die 1 bedeutet es ist erfüllbar und die 0 bedeutet es nicht erfüllbar bei (X1 V X2). Es muss also mind. eine 1 vorkommen, dass diese aussagenlogische Formel erfüllbar ist.

Gibt es also eine Möglichkeit, X mit den Werten 0 und 1 zu versehen und diese Anschließend wie oben in der Tabelle auszuwerten?


Vielen Dank schon mal für die Antwort.
 
Zuletzt bearbeitet:
Die Formelberechnung musst du ohne RegEx umsetzen. Oder höchstens die einzelnen Werte damit auslesen.
Die SAT kenne ich nicht. Da musst du ohne mich weiter kommen.
 
Zurück