kif/scheduling
2
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

added not on day and only on day constraint

Browse source
This commit is contained in:
Anja Reusch 2019-06-10 17:55:04 +02:00
parent c646051058
commit 3b33fcaad7
1 changed files with 70 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
generate_rules.py
View file

@ -1,13 +1,12 @@
import json import json
from math import floor from math import floor
import subprocess import subprocess
from collections import defaultdict
# Maximum time for AK: 2 Timeslots # Maximum time for AK: 2 Timeslots
SLOT_LEN = 120 SLOT_LEN = 120
DAYS = 1 DAYS = 3
START = 480 START = 480
END = 1200 END = 1200
@ -20,23 +19,35 @@ class WorkGroup:
self.projector = 'true' if projector else 'false' self.projector = 'true' if projector else 'false'
self.reso = 'true' if reso else 'false' self.reso = 'true' if reso else 'false'
self.length = floor(length / SLOT_LEN) + 1 self.length = floor(length / SLOT_LEN) + 1
if self.length > 2:
print(f"Warning, length of workgroup {id} greater than 2.")
self.length = 2
self.leaders = leaders self.leaders = leaders
self.constrainted_time = [] self.constrainted_time = [{'day': 1, 'time': 840, 'type': 'before'}] if reso else []
self.not_on_day = [] self.not_on_day = [0, 1, 2] if len(list(filter(lambda c: c['type'] == 'OnlyOnDay', constraints))) else []
if reso and not self.not_on_day:
self.not_on_day.append(2)
self.only_on_day = [] self.only_on_day = []
for constraint in constraints: for constraint in constraints:
if constraint["type"] == 'OnlyAfterTime': if constraint["type"] == 'OnlyAfterTime':
if constraint['workGroup'] is None: if constraint['workGroup'] is None:
self.constrainted_time.append({'day': constraint['day'], 'time': constraint['time'], 'type':'after'}) self.constrainted_time.append(
{'day': constraint['day'], 'time': constraint['time'], 'type': 'after'})
elif constraint["type"] == 'OnlyBeforeTime': elif constraint["type"] == 'OnlyBeforeTime':
self.constrainted_time.append({'day': constraint['day'], 'time': constraint['time'], 'type': 'before'}) self.constrainted_time.append({'day': constraint['day'], 'time': constraint['time'], 'type': 'before'})
elif constraint['type'] == 'NotOnDay':
print(self.constrainted_time) self.not_on_day.append(constraint['day'])
elif constraint['type'] == 'OnlyOnDay':
if constraint['day'] == 2 and reso:
print(f'WorkGroup {id}: only on day two, but has reso. Warning, is UNSATISFIABLE!')
self.not_on_day.remove(constraint['day'])
# TODO: more unsat warning when reso == True
def __str__(self): def __str__(self):
leader_rules = '' leader_rules = ''
for leader in self.leaders: for leader in self.leaders:
if leader.strip() != '':
leader_rules += f'leader({self.id}, "{leader}").\n' leader_rules += f'leader({self.id}, "{leader}").\n'
return f'ak({self.id}, {self.interest}, "{self.track}", {self.projector}, {self.reso}, {self.length}).\n' + leader_rules return f'ak({self.id}, {self.interest}, "{self.track}", {self.projector}, {self.reso}, {self.length}).\n' + leader_rules
@ -63,6 +74,7 @@ class Timeslot:
def __str__(self): def __str__(self):
return f'timeslot("{self.id}", {self.order}, {self.begin}, {self.end}, {self.day}).' return f'timeslot("{self.id}", {self.order}, {self.begin}, {self.end}, {self.day}).'
class Schedule: class Schedule:
def __init__(self, id, workgroup, day, time, room): def __init__(self, id, workgroup, day, time, room):
self.id = id self.id = id
@ -93,6 +105,7 @@ def parse_workgroups(data):
id_to_workgroup[workgroup['id']] = i id_to_workgroup[workgroup['id']] = i
return workgroups, id_to_workgroup return workgroups, id_to_workgroup
def parse_rooms(data): def parse_rooms(data):
rooms = [] rooms = []
id_to_room = {} id_to_room = {}
@ -112,8 +125,6 @@ data = json.load(open('backup.json'))
workgroups, id_to_workgroup = parse_workgroups(data) workgroups, id_to_workgroup = parse_workgroups(data)
rooms, id_to_room = parse_rooms(data) rooms, id_to_room = parse_rooms(data)
rules = """ rules = """
%LENGTH = { schedule(AK,TIMESLOT,ROOM): timeslot(TIMESLOT,_,_,_,_), room(ROOM,_,_) } :- ak(AK,_,_,_,_,LENGTH). %LENGTH = { schedule(AK,TIMESLOT,ROOM): timeslot(TIMESLOT,_,_,_,_), room(ROOM,_,_) } :- ak(AK,_,_,_,_,LENGTH).
LENGTH = { schedule(AK,TIMESLOT,ROOM): timeslot(TIMESLOT,_,_,_,_), room(ROOM,_,_) } :- ak(AK,_,_,_,_,LENGTH). LENGTH = { schedule(AK,TIMESLOT,ROOM): timeslot(TIMESLOT,_,_,_,_), room(ROOM,_,_) } :- ak(AK,_,_,_,_,LENGTH).
@ -141,17 +152,17 @@ for workgroup in workgroups:
for room in rooms: for room in rooms:
rules += str(room) + '\n' rules += str(room) + '\n'
timeslots = [(start, start + SLOT_LEN, day) for day in range(DAYS) for start in range(START, END, SLOT_LEN)] timeslots = [(start, start + SLOT_LEN, day) for day in range(DAYS) for start in range(START, END, SLOT_LEN)]
del timeslots[0] # remove slot thursday morning del timeslots[0] # remove slot thursday morning
if DAYS >= 3: del timeslots[-1] # remove last slot for Abschlussplenum if DAYS >= 3: del timeslots[-1] # remove last slot for Abschlussplenum
print(len(timeslots)) print(f'Number of Workgroups: {len(workgroups)}, Number of Rooms: {len(rooms)}, Number of Timeslots: {len(timeslots)}')
for order, timeslot in enumerate(timeslots): for order, timeslot in enumerate(timeslots):
if order == 8: if order == 8:
continue # remove slot for Resovorstellung, keep order to avoid two-slot-workgroups to be scheduled before and after reso. continue # remove slot for Resovorstellung, keep order to avoid two-slot-workgroups to be scheduled before and after Resovorstellung.
rules += str(Timeslot(order, timeslot)) + '\n' rules += str(Timeslot(order, timeslot)) + '\n'
############################ ############################
# ADD MORE CONSTRAINTS # # ADD MORE CONSTRAINTS #
############################ ############################
@ -160,33 +171,46 @@ def time_to_id(timeslots, day, time):
timeslots = list(filter(lambda ts: time >= ts[1][0] and time < ts[1][1] and day == ts[1][2], enumerate(timeslots))) timeslots = list(filter(lambda ts: time >= ts[1][0] and time < ts[1][1] and day == ts[1][2], enumerate(timeslots)))
return timeslots[0][0] return timeslots[0][0]
def get_last_on_day(day): def get_last_on_day(day):
if day == 0: if day == 0:
return 4 return 4
else: else:
return (day + 1) * 5 return (day + 1) * 5
def get_first_on_day(day): def get_first_on_day(day):
if day == 3: if day == 3:
return 15 return 15
else: else:
return (day) * 5 return (day) * 5
for workgroup in filter(lambda wg: wg.constrainted_time, workgroups):
for workgroup in workgroups:
if workgroup.constrainted_time:
for constrainted_time in workgroup.constrainted_time: for constrainted_time in workgroup.constrainted_time:
# TODO constraint for 2 slot workgroups missing! # TODO constraint for 2 slot workgroups missing!
timeslot_id = time_to_id(timeslots, constrainted_time['day'], constrainted_time['time']) timeslot_id = time_to_id(timeslots, constrainted_time['day'], constrainted_time['time'])
timeslot = timeslots[timeslot_id] # after this slot: ok timeslot = timeslots[timeslot_id] # after this slot: ok
operator1 = '<' if constrainted_time['type'] == 'after' else '>' operator1 = '<' if constrainted_time['type'] == 'after' else '>'
operator2 = '>' if constrainted_time['type'] == 'after' else '<' operator2 = '>' if constrainted_time['type'] == 'after' else '<'
day_restriction = get_last_on_day(constrainted_time['day']) + 1 if constrainted_time['type'] == 'before' else get_first_on_day(constrainted_time['day']) -1 #first or last slot on this day day_restriction = get_last_on_day(constrainted_time['day']) + 1 if constrainted_time[
'type'] == 'before' else get_first_on_day(
constrainted_time['day']) - 1 # first or last slot on this day
timeslot2 = timeslot_id if constrainted_time['type'] == 'before' else timeslot_id timeslot2 = timeslot_id if constrainted_time['type'] == 'before' else timeslot_id
print(f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER {operator1} {timeslot2}, ORDER {operator2} {day_restriction}.') print(
f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER {operator1} {timeslot2}, ORDER {operator2} {day_restriction}.')
rules += f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER {operator1} {timeslot2}, ORDER {operator2} {day_restriction}.\n' rules += f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER {operator1} {timeslot2}, ORDER {operator2} {day_restriction}.\n'
if workgroup.not_on_day:
for day in workgroup.not_on_day:
first_timeslot = get_first_on_day(day)
last_timeslot = get_last_on_day(day)
print(
f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER >= {first_timeslot}, ORDER <= {last_timeslot}.')
rules += f':- schedule({workgroup.id}, TIMESLOT, _), timeslot(TIMESLOT, ORDER, _, _, _), ORDER >= {first_timeslot}, ORDER <= {last_timeslot}.\n'
rules += "#show schedule/3." rules += "#show schedule/3."
####################### #######################
# GENERATE SCHEDULE # # GENERATE SCHEDULE #
####################### #######################
@ -212,6 +236,7 @@ if 'UNSATISFIABLE' in output:
else: else:
print('SATISFIABLE, outputting schedule...') print('SATISFIABLE, outputting schedule...')
import re import re
try: try:
match = re.match('(.|\n)*Answer: (.+)\n(.*)\nSATISFIABLE', output) match = re.match('(.|\n)*Answer: (.+)\n(.*)\nSATISFIABLE', output)
schedules_string = match.group(3) schedules_string = match.group(3)
@ -219,14 +244,14 @@ else:
print(e) print(e)
print(output) print(output)
schedules = [] schedules = []
from collections import defaultdict
workgroup_to_schedule = defaultdict(list) workgroup_to_schedule = defaultdict(list)
for i, schedule in enumerate(schedules_string.split('schedule')[1:]): for i, schedule in enumerate(schedules_string.split('schedule')[1:]):
match = re.match('\((.+),"(.+)#(.+)#.+",(.+)\)', schedule) match = re.match('\((.+),"(.+)#(.+)#.+",(.+)\)', schedule)
try: try:
workgroup_id = id_to_workgroup[int(match.group(1))] workgroup_id = id_to_workgroup[int(match.group(1))]
room_id = id_to_room[int(match.group(4))] room_id = id_to_room[int(match.group(4))]
schedules.append(Schedule(i, data['workGroups'][workgroup_id], match.group(2), match.group(3), data['rooms'][room_id])) schedules.append(
Schedule(i, data['workGroups'][workgroup_id], match.group(2), match.group(3), data['rooms'][room_id]))
# { # {
# 'id': i, # 'id': i,
# 'workGroup': data['workGroups'][workgroup_id], # 'workGroup': data['workGroups'][workgroup_id],
@ -256,7 +281,6 @@ else:
else: else:
schedules_filtered.append(schedules_for_workgroup_1) schedules_filtered.append(schedules_for_workgroup_1)
data = {} data = {}
data['schedules'] = [s.to_dict() for s in schedules_filtered] data['schedules'] = [s.to_dict() for s in schedules_filtered]
json.dump(data, open('output.json', 'w')) json.dump(data, open('output.json', 'w'))