Wettbewerb / Vergleich von Blockungsprogrammen

[Volker_Dirr]

hmm... Stimmt, Sie werden da nicht direkt EInfluss nehmen können. Der Solver ist der kritische Bereich. Ich habe gesehen, dass es da ja zig Versionen gibt. Alleine hier findet man sehr viele:
http://sat2018.forsyte.tuwien.ac.at/solvers/

da müsste ich aber viel testen

Haben Sie davon schon mehrere getestet? (Wenn ja: Welche? Dann würde ich mir evtl. mal die anderen testen)

[B. Bartsch]

Cryptominisat gehört zu den besten, auch Plingeling ist ganz gut. Die Top 10 unterscheiden sich in ihrer Qualität (Berechnungszeit) nur marginal.

[wschrewe]

Warum ist der neue Kurs42 Algorithmus noch nicht "offiziell"?

Weil der bisher ausführlich von zwei Leuten getestet wurde, und das ist IMHO etwas wenig, um ihn für die produktive Nutzung als Standard vorzugeben. Wir hoffen, dass jetzt durch die Möglichkeit, den neuen Algorithmus optional zu verwenden, verstärkt Rückmeldungen von "normalen" Benutzern kommen. Sie wissen als Programmierer selbst, dass man beim Test der eigenen Programme unterbewusst dazu neigt, kritische Stellen zu umgehen ...

[Volker_Dirr]

Ja, ist mir bekannt. Den Fall hatte ich auch direkt als Fall a) vermutet. Hätte ja auch Fall b) sein können.
Ich kann ihnen gerne Techniken schildern wie man das Problem automatisieren(minimieren) kann. Mache ich aber nur auf direkte Nachfrage um hier nicht zu stark vom Thema abzuweichen.

[wschrewe]

Ich kann ihnen gerne Techniken schildern wie man das Problem automatisieren(minimieren) kann.

Lieb von Ihnen. Ich habe auch schon mal gelesen, dass es sowas gibt. Wenn ich gar nicht mehr weiter weiß, melde ich mich.

[Volker_Dirr]

[...]Es ist also wenig Luft in den Blöcken. Ich habe in beiden Programmen ohne weitere Vorgaben geblockt (mit Ausnahme der beiden SuS, die nicht zusammen sollen, siehe Vorgaben.txt), und das kommerzielle Progamm kam auf KD4, während Kurs42 to CNF bei mir nur bis KD11 gekommen ist.

Ich habe eine neue Version veröffentlicht. Ich kann jetzt auch die Vorgabe "nicht zusammen mit" erfüllen.
Mit KD 3 und der "nicht zusammen mit"-Vorgabe habe ich 50 mal gemessen. Bester Fall 2 Sekunden. Langsamster Fall 770 Sekunden. Median 5 Sekunden.
siehe:
viewtopic.php?f=71&t=19&start=10#p13073

[wschrewe]

Der Download-Link funktioniert leider nicht.

[Volker_Dirr]

uppss.. verbessert.