Kurs42_To_CNF

Hier können alle Themen rund um die neuen zusätzlichen Blockungsprogramme diskutiert werden.

Moderator: wschrewe

NielsWestphal
Beiträge: 565
Registriert: Sonntag 2. Dezember 2018, 18:33
Schulform: Gymnasium

Re: Kurs42_To_CNF

Beitrag von NielsWestphal »

ok, dann kann es bei mir nicht schneller sein bei bis zu 12 parallelen Rechnungen...
mfg
Niels Westphal
B. Bartsch
Fachberater*in
Beiträge: 321
Registriert: Dienstag 4. Dezember 2018, 14:14
Schulform: Gymnasium

Re: Kurs42_To_CNF

Beitrag von B. Bartsch »

.... bei der 1. Berechnung ggf.

ABER bei der Auto-Optimierung nimmt man ja viele Einzelrechnungen (z.B. bei Strategie K). Und dann könnte Kissat schneller sein.

Ich habe mal eine Q1-Blockung genommen, mit Fixierung der LKs in Schiene 1-2, forciert max. LK-DIF = 5 und max. GK-DIF = 1. Alle Berechnungen mit einer 1 CPU von vorne (ohne Auto-Strategie).

Crypto: 848s, 488s, 69s, 274s ---> Schnitt 419s
Kissat: 57s, 275s, 155s, 229s, 101s, 348s, 25s, 75s, 11s, 201s --> Schnitt 147s

Man sieht allein daran, dass ich häufiger Kissat neugestartet habe, dass der Solver im Schnitt wohl schneller ist...

Ergänzung: Gibt man Crypto 8 Threads dann habe ich die Zeiten: 92s, 105s, 107s, 75s. D.h. bei der 1. Berechnung können mehrere Threads natürlich sehr nützlich sein. Ich hätte aber genausogut Kissat 8x startet können und dann die Zeit nehmen können, die die schnellste der 8 Berechnungen benötigte. Aus Neugier habe ich das mal gemacht und der schnellste (aus 8) benötigte 16s. Zufall? ;-)
Zuletzt geändert von B. Bartsch am Sonntag 20. Februar 2022, 21:32, insgesamt 2-mal geändert.
B. Bartsch
NielsWestphal
Beiträge: 565
Registriert: Sonntag 2. Dezember 2018, 18:33
Schulform: Gymnasium

Re: Kurs42_To_CNF

Beitrag von NielsWestphal »

ok, werde es mal testen.
mfg
Niels Westphal
Benutzeravatar
wschrewe
Fachberater*in
Beiträge: 1686
Registriert: Dienstag 25. September 2018, 17:36
Schulform: BK (Pensionär)
Kontaktdaten:

Re: Kurs42_To_CNF

Beitrag von wschrewe »

B. Bartsch hat geschrieben: Sonntag 20. Februar 2022, 20:35Kissat ist durchschnittlich schneller als cryptominisat.
Ich habe gesehen, dass Sie in Ihrem Paket cryptominisat5_nogauss vom 30.04.21 verwenden. Ich benutze seit einiger Zeit die Version von dieser Seite: https://github.com/msoos/cryptominisat/releases, und die ist um einiges schneller als die bisher benutzte Version von 2019.

Kissat werde ich gleich mal (mit Kurs 42 ;)) ausprobieren.
Mit freundlichen Grüßen
Walter Schrewe
"If all else fails, read the instructions" (Donald E. Knuth, letzter TeX - Hilfehinweis)
Benutzeravatar
wschrewe
Fachberater*in
Beiträge: 1686
Registriert: Dienstag 25. September 2018, 17:36
Schulform: BK (Pensionär)
Kontaktdaten:

Re: Kurs42_To_CNF

Beitrag von wschrewe »

Habe ich (mit einer Blockung, die mir ein freundlicher Kollege zur Verfügung gestellt hat). Mit den 75 definierten Regeln ergaben sich bei jeweils 5 Durchläufen für Kissat im Mittel 1' 34", für Cryptominisat 1' 54"". Es scheint, dass Krissat tatsächlich etwas schneller ist. Es waren bei beiden Solvern keine Optionen gesetzt, d.h. sie liefen mit ihren Default-Einstellungen.

Dann habe ich cryptominisat5 mit der Option --threads=4 gestartet. Hier ergibt sich nach 5 Durchläufen ein Mittel von (gerundet) 1' 14".

OT: Jetzt weiß ich nur noch nicht, was ich mit den gewonnenen 20 Sekunden anfangen soll...;)
Mit freundlichen Grüßen
Walter Schrewe
"If all else fails, read the instructions" (Donald E. Knuth, letzter TeX - Hilfehinweis)
B. Bartsch
Fachberater*in
Beiträge: 321
Registriert: Dienstag 4. Dezember 2018, 14:14
Schulform: Gymnasium

Re: Kurs42_To_CNF

Beitrag von B. Bartsch »

2022_04_13a
  • Neu: "Beenden?"-Abfrage beim Schließen des Fensters.
  • Neue Regel: Fach-Art#<...>#benötigt Ressource A#-
  • Neue Regel: Fach-Art#<...>#benötigt Ressource B#-
  • Neue Regel: Fach-Art#<...>#benötigt Ressource C#-
  • Neue Regel: Schiene#<...>#hat Ressource A maximal#<...>
  • Neue Regel: Schiene#<...>#hat Ressource B maximal#<...>
  • Neue Regel: Schiene#<...>#hat Ressource C maximal#<...>
Aufgrund von G9 werden ggf. einige Schulen vor dem Problem des Raum-Mangels stehen. Man kann dies bereits beim Blocken berücksichtigen (bis zu einem gewissen Grad). Die Idee ist, dass man pro Schiene beispielsweise maximal 3 Kurse erlaubt, die NICHT in einem Fachraum stattfinden. Wenn man das schafft, dann kann man der Stufe 3 feste Räume zuordnen, da pro Schiene maximal 3 Kurse gleichzeitig stattfinden, die einen "Klassenraum" benötigen. Ich habe mal eine alte Q1-Blockung genommen und folgenden Fach-Arten die Ressource A zugewiesen (A = Klassenraum).

Fach-Art#D;GK#benötigt Ressource A#-
Fach-Art#E5;GK#benötigt Ressource A#-
Fach-Art#ER;GK#benötigt Ressource A#-
Fach-Art#F6;GK#benötigt Ressource A#-
Fach-Art#GE;GK#benötigt Ressource A#-
Fach-Art#KR;GK#benötigt Ressource A#-
Fach-Art#L0;GK#benötigt Ressource A#-
Fach-Art#L6;GK#benötigt Ressource A#-
Fach-Art#M;GK#benötigt Ressource A#-
Fach-Art#PA;GK#benötigt Ressource A#-
Fach-Art#PL;GK#benötigt Ressource A#-
Fach-Art#S0;GK#benötigt Ressource A#-
Fach-Art#SW;GK#benötigt Ressource A#-

Danach habe ich ab Schiene 3 (Schiene 1-2 = LKs, habe ich ignoriert) zunächst alle Schienen auf 3x Ressource A begrenzt. Als es eine Lösung gab, habe ich schrittweise so viele Schienen wie möglich auf 2 reduziert. Das klappte drei Mal nicht (Schiene 9 bis 11).

LKs allein von Schiene#1#bis Schiene#2

Schiene#3#hat Ressource A maximal#2
Schiene#4#hat Ressource A maximal#2
Schiene#5#hat Ressource A maximal#2
Schiene#6#hat Ressource A maximal#2
Schiene#7#hat Ressource A maximal#2
Schiene#8#hat Ressource A maximal#2
Schiene#9#hat Ressource A maximal#3
Schiene#10#hat Ressource A maximal#3
Schiene#11#hat Ressource A maximal#3

Diese Blockung erlaubt es, der Stufe Q1 zwei bis drei Klassenräume fest zuzuordnen.

Beispielschiene (fett = benötigt Klassenraum):

Schiene 4 (92 SuS)
D-GK1 (19 SuS)
KU-GK3 (24 SuS)
PA-GK1 (24 SuS)
SP-GK4 (25 SuS)

.... soweit die Idee. Ob das wirklich sinnvoll ist, wird sich zeigen ;-)
B. Bartsch
Jaschke
Beiträge: 72
Registriert: Dienstag 28. Mai 2019, 11:52
Schulform: Gymnasium

Re: Kurs42_To_CNF

Beitrag von Jaschke »

Hallo,
ist es richtig, das beim Blocken der Q2 Kurswechsler von Kurs A nach B, wenn beide Kurse von der gleichen Lehrkraft unterrichtet werden, nicht mitgezählt werden?
Danke
Freundliche Grüße
Ansgar Jaschke
mian
Beiträge: 151
Registriert: Montag 10. August 2020, 21:28
Schulform: Gesamtschule

Regelwunsch: SchülerIn zusammen mit...

Beitrag von mian »

Hallo Benjamin,

wäre es denkbar, die Regel "SchülerIn zusammen mit SchülerIn" einzubauen?
--
Mit besten Grüßen
Michael Andres
A.Siebert
Beiträge: 6
Registriert: Montag 21. Februar 2022, 18:15
Schulform: GY

Re: Kurs42_To_CNF

Beitrag von A.Siebert »

Sehr geehrter Herr Bartsch,

vielen Dank, dass Sie uns die vielen hilfreichen Tools zur Verfügung stellen!
Auf meinem Windows-PC in der Schule konnte ich den Konferenzplaner erfolgreich installieren, daheim scheitere ich gerade daran, auf meinem Macdas Hilfsprogramm "cryptominisat" zu kompilieren.

Die Homebrew-Umgebung habe ich erfolgreich installiert. Nach der Eingabe im Terminal von
brew install cmake boost zlib
tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-version
mkdir build && cd build
cmake ..
make
sudo make install

erhalte ich die Fehlermeldung

"make: *** No rule to make target `install'. Stop" und das Programm bricht ab.

Was mache ich falsch?

Herzliche Grüße aus Oberhausen
Alexander Siebert
Antworten

Zurück zu „Externe Blockungsprogramme“