Kurs42_To_CNF
Moderator: wschrewe
-
- Beiträge: 572
- Registriert: Sonntag 2. Dezember 2018, 18:33
- Schulform: Gymnasium
Re: Kurs42_To_CNF
ok, dann kann es bei mir nicht schneller sein bei bis zu 12 parallelen Rechnungen...
mfg
Niels Westphal
Niels Westphal
-
- Fachberater*in
- Beiträge: 321
- Registriert: Dienstag 4. Dezember 2018, 14:14
- Schulform: Gymnasium
Re: Kurs42_To_CNF
.... 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?
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
-
- Beiträge: 572
- Registriert: Sonntag 2. Dezember 2018, 18:33
- Schulform: Gymnasium
- wschrewe
- Fachberater*in
- Beiträge: 1700
- Registriert: Dienstag 25. September 2018, 17:36
- Schulform: BK (Pensionär)
- Kontaktdaten:
Re: Kurs42_To_CNF
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.B. Bartsch hat geschrieben: ↑Sonntag 20. Februar 2022, 20:35Kissat ist durchschnittlich schneller als cryptominisat.
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)
Walter Schrewe
"If all else fails, read the instructions" (Donald E. Knuth, letzter TeX - Hilfehinweis)
- wschrewe
- Fachberater*in
- Beiträge: 1700
- Registriert: Dienstag 25. September 2018, 17:36
- Schulform: BK (Pensionär)
- Kontaktdaten:
Re: Kurs42_To_CNF
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...
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)
Walter Schrewe
"If all else fails, read the instructions" (Donald E. Knuth, letzter TeX - Hilfehinweis)
-
- Fachberater*in
- Beiträge: 321
- Registriert: Dienstag 4. Dezember 2018, 14:14
- Schulform: Gymnasium
Re: Kurs42_To_CNF
2022_04_13a
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
- 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#<...>
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
Re: Kurs42_To_CNF
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
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
Ansgar Jaschke
Regelwunsch: SchülerIn zusammen mit...
Hallo Benjamin,
wäre es denkbar, die Regel "SchülerIn zusammen mit SchülerIn" einzubauen?
wäre es denkbar, die Regel "SchülerIn zusammen mit SchülerIn" einzubauen?
--
Mit besten Grüßen
Michael Andres
Mit besten Grüßen
Michael Andres
Re: Kurs42_To_CNF
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
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