Seite 4 von 4

Re: Kurs42_To_CNF

Verfasst: Sonntag 20. Februar 2022, 20:56
von NielsWestphal
ok, dann kann es bei mir nicht schneller sein bei bis zu 12 parallelen Rechnungen...

Re: Kurs42_To_CNF

Verfasst: Sonntag 20. Februar 2022, 21:07
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? ;-)

Re: Kurs42_To_CNF

Verfasst: Sonntag 20. Februar 2022, 21:26
von NielsWestphal
ok, werde es mal testen.

Re: Kurs42_To_CNF

Verfasst: Montag 21. Februar 2022, 11:04
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.

Re: Kurs42_To_CNF

Verfasst: Montag 21. Februar 2022, 12:29
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...;)

Re: Kurs42_To_CNF

Verfasst: Mittwoch 13. April 2022, 12:44
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 ;-)

Re: Kurs42_To_CNF

Verfasst: Montag 16. Mai 2022, 23:10
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

Regelwunsch: SchülerIn zusammen mit...

Verfasst: Donnerstag 16. März 2023, 11:35
von mian
Hallo Benjamin,

wäre es denkbar, die Regel "SchülerIn zusammen mit SchülerIn" einzubauen?

Re: Kurs42_To_CNF

Verfasst: Montag 30. Oktober 2023, 18:23
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