3-SAT, ein paar Grundsatzfragen

[Daniel A. (daniel-a)]

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.

[Michael S. (bitpulse)]

...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)

[Peter D. (peda)]

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.

[Cyblord -. (Gast)]

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 ?

[Daniel A. (daniel-a)]

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:

function genRandom3SAT(){
  var s = "abcdefghijklmnopqrstuvwxyz";
  const randvar = () => (Math.random() > 0.5 ? '!' : '') + s[Math.round( (s.length - 1) * Math.pow(Math.random(), 2) )];
  var termcount = Math.round( Math.random() * 20 + 1 );
  var a = [];
  while(termcount--)
    a.push([randvar(),randvar(),randvar()])
  return a;
}

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:

function get3SAT3VarConfiguration(i,v1=1,v2=2,v3=3){
  var n1 =  i       & 1;
  var n2 = (i >> 1) & 1;
  var n3 = (i >> 2) & 1;
  return [
    v1 ? (n1?'!':'') + v1 : 0,
    v2 ? (n2?'!':'') + v2 : 0,
    v3 ? (n3?'!':'') + v3 : 0
  ];
}

function* gen3SAT(v=1, i=0, j=0, k=0, m=0){
  var vars = [];
  for(var vi=0; vi<v; vi++)
    vars.push(Array.from(vi.toString(26)).map(x=>(parseInt(x,26)+10).toString(36)).join(''));
  while(true){
    var c = [];
    for(let l=0; l<vi; l++){
      c.push(get3SAT3VarConfiguration(m,vars[i],vars[j],vars[k]));
      m++;
      if(m>=8)  m=0, i++;
      if(i>=vi) i=0, j++;
      if(j>=vi) j=0, k++;
      if(k>=vi){
        k = 0;
        vars.push(Array.from(vi.toString(26)).map(x=>(parseInt(x,26)+10).toString(36)).join(''));
        vi += 1;
      }
    }
    yield [c,vi,i,j,k,m];
  }
}

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.