Schulverwaltungssoftware NRW

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)

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

Volker_Dirr hat geschrieben: Samstag 27. Juni 2020, 07:16Warum 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 ...

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.

Volker_Dirr hat geschrieben: Samstag 27. Juni 2020, 15:22Ich 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.

Falko Müller hat geschrieben: Montag 22. Juni 2020, 09:42 [...]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

Der Download-Link funktioniert leider nicht.

uppss.. verbessert.