Hallo zusammen! Ich dachte mir ich versuche mal so zum spass das 3-SAT Problem zu lösen, bzw. einen Algorithmus zu finden, der alle 3-SAT Probleme in Polynomischer Zeit lösen kann, einfach mal um zu sehen, wie weit ich komme. Ich implementiere dass dann direkt als Funktion in einem Programm, damit ich gleich ausprobieren kann, ob ich irgendwelche offensichtlichen Fehler gemacht habe. Nun stellen sich mir einige Grundlagefragen: 1) Bei 3-SAT, muss ich dort nur für jedes Problem sagen können: a) ob lösungen existieren (also das Resultat nicht immer false ist) b) oder muss ich mindestens eine konkrete Lösung finden c) oder muss mein Algorithmuss sogar Alle lösungen finden? 2) Bei der O-Notation, soll ich bei Zuweisungen, beim Inkrementieren von Variablen und bei Vergleichen von O(1) oder von O(n) ausgehen? Der Wertebereich wird bei meinen Ansätzen vermutlich eine Lineare, vielleicht höchstens mal eine Quadratische relation zur Anzahl Variablen haben. (Wobei ich bei meiner Implementation eine Fixe grösse verwenden werde, weil der addressierbare Speicher meines PCs sowieso begrenzt ist, und ich damit das Maximum für diesen kenne) 3) Wenn ich es schaffen sollte, 3-SAT so zu lösen, würde das Bedeuten dass P=NP, und damit hätte ich eines der Millennium Prize Problems gelöst, worauf ein Gewinn von 1 Mio. ausgeschrieben wurde, korrekt? 4) Sollte ich eine lösung finden, wie gebe ich das am besten bekannt, ohne dass jemand anderes diese als seine eigene ausgeben kann? Einfach hier im Forum Posten? Oder besser in mehreren? PS: Ich weiss, dass ich vermutlich keine Lösung finden werde, aber es macht trotzdem spass, das Problem immer weiter herunterzubrechen und immer mehr Fälle abzudecken.
...na wenn du jetzt schon weist das du die Lösung nicht finden wirst - ich finde das sind die allerbesten Vorraussetzungen, viel Spaß noch ! oder du rufst mal jemand an der sich damit auskennt :-) (06131/70-16578)
Angehängte Dateien:
-
3sat.JPG
(9,9 KB)
Für die Lösung von Logikgleichungen die eierlegende Wollmilchsau zu erfinden, mag interessant klingen, in der Praxis sind die Aufgaben aber wesentlich einfacher gestrickt. Z.B. hat man für 7-Segmentdekoder nur die Kombinationen für 0..9 gelöst, daher hat der 74HC47 bei A..F wirre Ausgaben. Dein Punkt c) wurde also nicht erfüllt. In FPGAs wird oft eine LUT verwendet, d.h. man muß Logikgleichungen nicht auflösen. Die LUT erhält alle Eingangskombinationen als Adresse.
Gast
#5517230
Du solltest erstmal am exakten wording arbeiten und dann eine Theo. Inf. Vorlesung besuchen. Es gibt nicht die 3sat Probleme sondern nur das 3sat Problem und Probleme die darauf reduzierbar sind ?
Abradolf L. schrieb: > Du solltest erstmal am exakten wording arbeiten und dann eine Theo. Inf. > Vorlesung besuchen. Theo. Inf. Vorlesung für ein bisschen boolesche Algebra? Ein paar Papierblöcke, etwas zum Schreiben und ein paar Jahre Erfahrung mit Programme schreiben und die damit verbundenen Logikprobleme zu lösen reicht doch völlig. Die Ausdrucksweise zu verbessern könnte Sinn machen, aber nur für so ein paar Fragen in diesem Forum erschien mir das nicht nötig. > Es gibt nicht die 3sat Probleme sondern nur das 3sat > Problem und Probleme die darauf reduzierbar sind ? Schon klar. Mit den Problemen meinte ich in konjunktiver Normalform vorliegende aussagenlogische Formeln, die höchstens 3 Literale pro Klausel enthalten. Aber das macht die Sätze nur Komplizierter, wenn ich das immer so schreiben würde, und am Ende wüssten die Leser doch noch weniger was gemeint war als zuvor. Oder hast du eine bessere Idee, wie man das Bezeichnen könnte? Bei gewissen Artikeln, die ich gelesen habe, wurden auf diese nur als ein 3-SAT Bezug genommen, ist das besser? Momentan ist mein Hauptproblem, gute Testfälle für meinen Solver zu generieren. Der Solver selbst scheint schon recht vielversprechende Resultate zu liefern. Bisher habe ich folgendes versucht: Zufällige Formeln generieren:
1 | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
Das Problem damit ist nur, das ich damit von 200'000 fällen nur so rund 5 habe, die keine Lösung haben. Ausserdem kann es dazu kommen, das ich mehrmals den gleichen Fall bekomme, und viele werden ausgelassen. Das ist nicht wirklich geeignet, um den Solver zuverlässig zu testen. Das Ding muss Stunden laufen, bis es vielleicht mal einen unscheinbaren kleinen Fehler im Solver aufdeckt. Ich bräuchte etwas, wo ich alle Relevanten Kombinationen mal durchlaufen kann. Ich hab mal mit soeinem generator versucht:
1 | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
10 | |
11 | |
12 | |
13 | |
14 | |
15 | |
16 | |
17 | |
18 | |
19 | |
20 | |
21 | |
22 | |
23 | |
24 | |
25 | |
26 | |
27 | |
28 | |
29 | |
30 | |
31 | |
32 | |
Aber das funktioniert leider auch nicht so wie es soll. Nach ein paar tausend Kombinationen generiert es nurnoch unlösbare fälle, und immer aus dem gleichen Grund unlösbare. Das ist noch unbrauchbarer als die zufälligen. Aber wenigstens kann man es dort fortsetzen, wo man zuletzt aufgehört hat. Hat jemand eine Idee, wie man bessere und möglichst vielfältige Testfälle generieren kann? Fälle wie z.B. doppelte Klauseln, Klauseln die gleich zu 1 werden (z.B. a||!a), und Fälle wo nur die Variablnamen anders sind, etc. sind zwar kein Problem, aber zum Testen nicht wirklich sinvoll. Ein paar spezifische Testfälle, um edge cases zu testen, habe ich bereits.