diff options
author | Peter Wu <peter@lekensteyn.nl> | 2016-12-14 22:28:59 +0100 |
---|---|---|
committer | Peter Wu <peter@lekensteyn.nl> | 2016-12-14 22:28:59 +0100 |
commit | 079f4e83761c34ada419e0fd3d4642ba5b922d3c (patch) | |
tree | c1a0b3150271ebd5bdc81c45f65c9e5f6bf44858 /job_scheduling/generate-jobscheduling.py | |
parent | f06f3da571d2785c0c7753a1c4b33e75cbd8936b (diff) | |
download | 2IMF25-AR-079f4e83761c34ada419e0fd3d4642ba5b922d3c.tar.gz |
JobScheduling: redo 3a
The report was too terse and incomplete. For example, the included code
was missing checks for the minimal time and the Java code contains a
strange check for the last constraint that seems wrong (did you mean
"or"?).
Just redo it, saves more time.
Also, the generate-jobscheduling.py scrypt contains dead code. I
originally planned to implement marking dependencies, but that is not
done.
Diffstat (limited to 'job_scheduling/generate-jobscheduling.py')
-rwxr-xr-x | job_scheduling/generate-jobscheduling.py | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/job_scheduling/generate-jobscheduling.py b/job_scheduling/generate-jobscheduling.py new file mode 100755 index 0000000..5cf9b04 --- /dev/null +++ b/job_scheduling/generate-jobscheduling.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python +# Usage for 3a (first argument is the deadline): +# $0 -1 | z3 -smt -in +# Usage for 3b: +# $0 90 b | z3 -smt -in + +import sys + +# Deadline +deadline = int(sys.argv[1]) +is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b' + + +# Number of jobs +n = 12 + +# For i: (j, ...), job i must not start before jobs j have ended. +job_dependencies_ended = { + 3: (1, 2), + 5: (3, 4), + 7: (3, 4, 6), + 9: (5, 8), + 11: (10,), + 12: (9, 11), +} + +job_dependencies_started = { + 8: (5,), +} + +job_durations = { + i: i + 5 for i in range(1, n + 1) +} + + +def fillin(cases, template_vars): + if type(cases) == str: + return cases.format(**template_vars) + return [template.format(**template_vars) for template in cases] + +literals = [] +preds = [] + +# Start time of all jobs +# and their duration +for i in range(1, n + 1): + literals += fillin([ + "t{i}", + "d{i}", + ], vars()) + # times must be positive and + # all jobs must finish before the deadline. + preds += fillin([ + "(>= t{i} 0)", + "(<= (+ t{i} d{i}) {deadline})", + ], vars()) + +# Define duration +for i, duration in job_durations.items(): + preds += fillin([ + "(= d{i} {duration})" + ], vars()) + +# Job i may not start before job(s) j have *ended*. Or: +# for all j: t_j + d_j <= t_i +for i, deps in job_dependencies_ended.items(): + for j in deps: + preds += fillin([ + "(<= (+ t{j} d{j}) t{i})" + ], vars()) + +# Job i may not start before job(s) j have *started*. Or: +# for all j: t_j <= t_i +for i, deps in job_dependencies_started.items(): + for j in deps: + preds += fillin([ + "(<= t{j} t{i})" + ], vars()) + +# Jobs 5, 7 en 10 require a special equipment of which only one copy is +# available, so no two of these jobs may run at the same time. +# Or: +# There must exist a pair of jobs (i, j) s.t. one starts after another ended: +# t_i + d_i <= t_j +jobs_max2_for_3 = (5, 7, 10) +altpreds = [] +for i in jobs_max2_for_3: + for j in jobs_max2_for_3: + if i == j: + continue + altpreds += fillin([ + "(<= (+ t{i} d{i}) t{j})" + ], vars()) + +preds += ["(or %s)" % " ".join(altpreds)] + +# Begin generator +s = """(benchmark test.smt +:logic QF_UFLIA +:extrafuns +( +""" +s += "\n".join("(%s Int)" % x for x in literals) +s += """ +) +:formula +(and +""" +s += "\n".join(preds) +s += """ +)) +""" + +try: + import sys + print(s) + # Hack to avoid printing a ugly error in case stdin of next pipe is closed. + sys.stdout.flush() + sys.stdout.close() +except BrokenPipeError: + pass |