2016-03-28 12 views
0

Anders als eine Ausgabedatei erzeugen, dann mit wc -l output.txt und -1 dividiere durch 2 und Kopf -50 die output.txt, gibt es einen einfachen Weg auto no Anzahl der Lösung in minizinc zählen und die erste 50 Lösung drucken? Mein Programm lief für 12 Stunden in einem Szenario und das andere sollte 2 Tage laufen!Minizinc - Nummer der Lösung zählen und erste 50 nur für die Überprüfung drucken

Auch eine Möglichkeit, im Batch-Modus (nicht ide) Ressourcen Nutzung andere als die Verwendung von Zeit minizinc ...

Vielen Dank für Beratung

+0

Sie benötigen dafür ein drittes Programm. Vorzugsweise kann etwas, das einen Stream (stdout) lesen und ein Symbol zählen kann und sobald 50 erreicht ist, das Programm abbrechen. Ich bin mir nicht sicher, ob ein Befehlszeilenprogramm das kann und Sie vielleicht ein Skript in einer echten Programmiersprache benötigen. – Kobbe

+0

Kann nicht abgebrochen werden, da immer noch die Anzahl der Lösungen gezählt werden muss. Nur um zu vermeiden, 2 GB + Log-Datei zu generieren (es ist ein + als das einfache Modell 12 Stunden + zu beenden und ich denke, nie lange genug zu warten. Ich wusste nur die Lösung für die Herausforderung dauert nur 1,5 Minuten mit Node.js) . Versuchen Sie nicht aufzugeben, aber ... –

+0

Aber MiniZinc druckt die Lösungen auf stdout, wenn es sie findet. Starten Sie MiniZinc im Kommandozeilenmodus mit http://stackoverflow.com/questions/2804543/read-subprocess-stdout-line-by-line und lesen Sie die Ausgabe in Echtzeit. Sobald Sie Ihre 50 Lösungen gefunden haben, beenden Sie den Subprozess. – Kobbe

Antwort

1

Das Kommandozeilenprogramm „minizinc“ sowie die meisten FlatZinc zu erzeugen Solver unterstützt den Parameter "-n", der die Anzahl der anzuzeigenden Lösungen angibt. Die MiniZinc IDE hat die Option "Nach vielen Lösungen stoppen:".

Beachten Sie, dass dies für Zufriedenheitsprobleme relevant ist. Für Optimierungsprobleme gibt es jedoch keinen Konsens darüber, wie verschiedene Solver mit "-n" umgehen.