Wer kann mir eine Einführung in die Benutzung von SAT-Solvern geben? Ich habe eine Reihe von boolschen Gleichungen und möchte diese Lösen. Ev. Bezahlung möglich.
Hallo,
CNF-SAT? Und brauchst Du da noch eine Sprache herum, a la Prolog oder z3? Oder reicht eine Bibliothek mit Algorithmen?
Oh, und die ungefähre Größe des Problems wäre noch interessant.
Hallo,
also es geht mir hauptsächlich um die Frage, ob ich eine Reihe von Gleichungen in die KNF bringen kann, um das dann von einem SAT-Solver lösen zu lassen. Die Gleichungen enthalten immer IF-Klauseln, wie z.B.
-1=(IIf(V65859V=-1,IIf(V12751V=-1,V65922V,NOT(V65922V)),IIf(V12751V=-1,NOT(V65922V),V65922V)));
V65924V=(IIf(V65859V=-1,IIf(V12751V=-1,-1,IIF(V65922V=-1,-1,0)),IIf(V12751V=-1,IIf(V65922V=-1,-1,0),0)));
-1=(IIf(V65861V=-1,IIf(V12753V=-1,V65924V,NOT(V65924V)),IIf(V12753V=-1,NOT(V65924V),V65924V)));
V65926V=(IIf(V65861V=-1,IIf(V12753V=-1,-1,IIF(V65924V=-1,-1,0)),IIf(V12753V=-1,IIf(V65924V=-1,-1,0),0)));
Die Variablen sind immer in der Form: „V“ + Nummer + „V“. Also z.B. V65859V
Es sind ca. 60.000 Gleichungen und in etwa gleich viele Variablen. Man könnte theoretisch die Variablen substituieren, aber dann erhält man eine Formel, die die Kapazitäten des Rechners überschreitet. Daher meine Idee, diese Gleichungen durch einen SAT-Solver lösen zu lassen. Danke im Voraus für eine Antwort.
Ja, das habe ich mir fast gedacht. Die meisten Solver (außerhalb von Programmierumgebungen) wollen CNF (KNF auf deutsch). Die Umwandlung ist eigentlich sehr mechanisch und ist oft Aufgabe von Programmierübungen an den Unis. Ich kenne auf Anhieb keine Software-Lösung, die ausschließlich darauf abgestellt ist. Ist vielleicht zu einfach?
Ich nehme immer die CLP(X)-Solver meiner Prolog-Installation (SWI-Prolog), CLP(Z_2) ist identisch mit SAT. Prolog hat den Vorteil, daß man sich Identitäten wie
ExactlyOne(P,Q) :- P*-Q + -P*Q
definieren kann, und damit dann in diesen Identitäten das Problem formulieren kann. Die interne Darstellung ist mir dann egal.
Für 60000 Variablen nimmt man aber besser einen spezialisierten Solver, Prolog mit Backtracking geht bis ca. 1000 noch ganz gut. 60000 dürfte aber schon mehrere Tage/Wochen/Monate dauern, und vermutlich irgendwann fehlschlagen.