CNF-Blockung?

[Meike Klingauf]

Guten Abend,
mit dem Herunterladen des aktuellen kursSnapshot (Version 3.33.39.532) bekommt man ein .pdf mit Namen "CNF-Solver". Dort heißt es
"Erreicht wird die Funktionalität über den Menüpunkt Blocken→CNFBlockung. Es öffnet sich der folgende Dialog:"...

Ist das aktuell? Bei dem Menüpunkt "Blocken" sehe ich nur das Übliche, "Automaatisch Blocken" etc.

Ich würde sehr gerne mit dem integrierten CNF-Solver blocken, bin ein großer Fan von dem ehemaligen "bar_Kurs42_To_CNF", herzliche Grüße an Herrn Bartsch!

Danke für Auskünfte
Meike Klingauf

[NielsWestphal]

Wieso "ehemalig" ?

[Meike Klingauf]

Hallo Herr Westphal, danke.
Ich habe die Version "bar_Kurs42_To_CNF_2022_04_13a" und ging davon aus, dass Herr Bartsch das Programm nicht mehr weiter pflegt, weil es jetzt "Kurs 42 mit integriertem CNF-Solver" (zitiert aus dem oben genannten.pdf) gibt?

Die "bar_Kurs42_To_CNF"-Software erzeugt bei mir bei "Debug": Cannot run program "": CreateProcess error=87, Falscher Parameter

Das eine oder das andere - ich möchte gerne mit den Regeln blocken, die ich selbst setzen kann.

Grüße
Meike Klingauf

[wschrewe]

Ist das aktuell? Bei dem Menüpunkt "Blocken" sehe ich nur das Übliche, "Automaatisch Blocken" etc.

Ja. Sie müssen das CNF-Blocken über "Extras->Einstellungen->Allgemeines->Blockung optimieren" aktivieren.

CNF-Einstellung.png (6.62 KiB) 406 mal betrachtet

Nach einem Neustart von Kurs 42 steht der Menüpunkt zur Verfügung.

[Meike Klingauf]

Hallo Herr Schrewe,
das funktioniert, und ich bekomme ein "s SATISFIABLE". Rechts habe ich aber die Schaltfläche "Ergebnis übernehmen" nicht, nur die anderen drei Schaltflächen, die dort auch hingehören (Neuer Tab, Tab schließen und Ende). Haben Sie hierzu auch eine Lösung? Ich hoffe es sehr...

Danke und einen schönen Tag
Meike Klingauf

[wschrewe]

aben Sie hierzu auch eine Lösung? Ich hoffe es sehr...

Rechte Maustaste im Ergebnis-Tab->Ergebnis übernehmen

[NielsWestphal]

Ich verwende das Programm in der Version 2022_02_20a und mit der neuesten Cryptominisat Version. Läuft alles. Ich finde es sehr komfortabel, die Regeln über Copy&Paste dort immer wieder unterzubringen.

[NielsWestphal]

Die aktuelle Version von CNF wird aber zumindest hier im Forum nicht mehr zum Download angeboten. Oder übersehe ich etwas?

[wschrewe]

Ich finde es sehr komfortabel, die Regeln über Copy&Paste dort immer wieder unterzubringen.

Geht in Kurs genau so. Man kann die Regeln auch in einer Textdatei speichern und wieder laden. Ich werde die neueste Cryptominisat-Version mal ausprobieren. Bei meinen bisherigen Tests war Kissat etwas schneller.

[wschrewe]

Ich werde die neueste Cryptominisat-Version mal ausprobieren.

Habe ich gemacht. Die neueste Version ist (bei meiner Testblockung) mehr als doppelt so schnell wie Kissat!