307 lines
12 KiB
Python
307 lines
12 KiB
Python
import json
|
|
from math import floor
|
|
import subprocess
|
|
from collections import defaultdict
|
|
|
|
# Maximum time for AK: 2 Timeslots
|
|
SLOT_LEN = 120
|
|
|
|
DAYS = 3
|
|
START = 480
|
|
END = 1200
|
|
|
|
|
|
class WorkGroup:
|
|
def __init__(self, id, interest, track, projector, reso, length, leaders, constraints):
|
|
self.id = id # must be int
|
|
self.interest = interest
|
|
self.track = track if track is not None else 'none' # haben alle aks einen track?
|
|
self.projector = 'true' if projector else 'false'
|
|
self.reso = 'true' if reso else 'false'
|
|
self.length = floor((length-1) / SLOT_LEN) + 1
|
|
# if self.length > 2:
|
|
# print(f"Warning, length of workgroup {id} greater than 2.")
|
|
# self.length = 2
|
|
self.leaders = leaders
|
|
self.constrainted_time = [{'day': 1, 'time': 840, 'type': 'before'}] if reso else []
|
|
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 = []
|
|
|
|
for constraint in constraints:
|
|
if constraint["type"] == 'OnlyAfterTime':
|
|
if constraint['workGroup'] is None:
|
|
self.constrainted_time.append(
|
|
{'day': constraint['day'], 'time': constraint['time'], 'type': 'after'})
|
|
elif constraint["type"] == 'OnlyBeforeTime':
|
|
self.constrainted_time.append({'day': constraint['day'], 'time': constraint['time'], 'type': 'before'})
|
|
elif constraint['type'] == 'NotOnDay':
|
|
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):
|
|
leader_rules = ''
|
|
for leader in self.leaders:
|
|
if leader.strip() != '':
|
|
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
|
|
|
|
|
|
class Room:
|
|
def __init__(self, id, n_places, projector, is_pool): # TODO internet, whiteboard & co.
|
|
self.id = id # must be int
|
|
self.n_places = n_places
|
|
self.projector = 'true' if projector else 'false'
|
|
self.is_pool = is_pool
|
|
|
|
def __str__(self):
|
|
pool_rule = ''
|
|
if self.is_pool:
|
|
pool_rule = f'\npool({self.id}).'
|
|
return f'room({self.id}, {self.n_places}, {self.projector}).{pool_rule}'
|
|
|
|
|
|
class Timeslot:
|
|
def __init__(self, order, timeslot):
|
|
self.begin, self.end, self.day = timeslot
|
|
self.id = f'{self.day}#{self.begin}#{self.end}'
|
|
self.order = order
|
|
# self.begin = begin
|
|
# self.end = end
|
|
# self.day = day
|
|
|
|
def __str__(self):
|
|
return f'timeslot("{self.id}", {self.order}, {self.begin}, {self.end}, {self.day}).'
|
|
|
|
|
|
class Schedule:
|
|
def __init__(self, id, workgroup, day, time, room):
|
|
self.id = id
|
|
self.workgroup = workgroup
|
|
self.room = room
|
|
self.day = day
|
|
self.time = time
|
|
|
|
def to_dict(self):
|
|
return {
|
|
'id': self.id,
|
|
'workGroup': self.workgroup,
|
|
'room': self.room,
|
|
'time': self.time,
|
|
'day': self.day,
|
|
'lockRoom': False,
|
|
'lockTime': False,
|
|
}
|
|
|
|
|
|
def parse_workgroups(data):
|
|
workgroups = []
|
|
id_to_index_workgroup = {}
|
|
for i, workgroup in enumerate(data['workGroups']):
|
|
workgroups.append(
|
|
WorkGroup(workgroup['id'], workgroup['interested'], workgroup['track'], workgroup['projector'],
|
|
workgroup['resolution'], workgroup['length'], workgroup['leader'], workgroup['constraints']))
|
|
id_to_index_workgroup[workgroup['id']] = i
|
|
return workgroups, id_to_index_workgroup
|
|
|
|
|
|
def parse_rooms(data):
|
|
rooms = []
|
|
id_to_room = {}
|
|
for i, room in enumerate(data['rooms']):
|
|
rooms.append(Room(room['id'], room['places'], room['projector'], room['pool'])) # TODO internet, whiteboard & co.
|
|
id_to_room[room['id']] = i
|
|
return rooms, id_to_room
|
|
|
|
|
|
#######################
|
|
# READ BACKUP JSON #
|
|
#######################
|
|
|
|
|
|
data = json.load(open('backup.json'))
|
|
|
|
workgroups, id_to_index_workgroup = parse_workgroups(data)
|
|
rooms, id_to_index_room = parse_rooms(data)
|
|
|
|
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).
|
|
|
|
% forbid 2AKS in the same room at the same time
|
|
:- schedule(AK1,TIMESLOT,ROOM), schedule(AK2,TIMESLOT,ROOM), AK1 != AK2.
|
|
|
|
% forbid ak with beamer request in room without beamer
|
|
:- schedule(AK,_,ROOM), ak(AK,_,_,true,_,_), room(ROOM,_,false).
|
|
|
|
% forbid ak in room that is too small
|
|
:- schedule(AK,_,ROOM), ak(AK,INTEREST,_,_,_,_), room(ROOM,PLACES,_), PLACES<INTEREST.
|
|
|
|
% forbid two AKs with same leader at same timestep
|
|
:- schedule(AK1,TIMESTEP,_), schedule(AK2,TIMESTEP,_), leader(AK1,LEADER), leader(AK2,LEADER), AK1 != AK2.
|
|
|
|
% schedules of longer aks should be in the same room and in consecutive timeslots, on the same day
|
|
%schedule(AK,TIMESLOT2,ROOM) :- ak(AK,_,_,_,_,LENGTH), LENGTH>1, schedule(AK,TIMESLOT1,ROOM), timeslot(TIMESLOT1,ORDER1,_,_,DAY), timeslot(TIMESLOT2,ORDER2,_,_,DAY), timeslot(TIMESLOT3,ORDER3,_,_,_), ORDER2 != ORDER1+1, ORDER1 = ORDER3+1, not schedule(AK,TIMESLOT3,ROOM) .
|
|
:- schedule(AK, TIMESLOT1, _), schedule(AK, TIMESLOT2, _), timeslot(TIMESLOT1,ORDER1,_,_,_), timeslot(TIMESLOT2,ORDER2,_,_,_), ak(AK,_,_,_,_,LENGTH), |ORDER2-ORDER1| >= LENGTH.
|
|
%same room
|
|
:- schedule(AK, _, ROOM1), schedule(AK, _, ROOM2), ROOM1 != ROOM2.
|
|
%same day
|
|
:- schedule(AK, TIMESLOT1, _), schedule(AK, TIMESLOT2, _), timeslot(TIMESLOT1, _,_,_, DAY1), timeslot(TIMESLOT2, _,_,_, DAY2), DAY1 != DAY2.
|
|
"""
|
|
lengths = defaultdict(int)
|
|
for workgroup in workgroups:
|
|
lengths[workgroup.length] += 1
|
|
rules += str(workgroup) + '\n'
|
|
|
|
print(lengths)
|
|
|
|
for room in rooms:
|
|
rules += str(room) + '\n'
|
|
|
|
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
|
|
if DAYS >= 3: del timeslots[-1] # remove last slot for Abschlussplenum
|
|
print(f'Number of Workgroups: {len(workgroups)}, Number of Rooms: {len(rooms)}, Number of Timeslots: {len(timeslots)}')
|
|
for order, timeslot in enumerate(timeslots):
|
|
if order == 8:
|
|
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'
|
|
|
|
|
|
############################
|
|
# ADD MORE CONSTRAINTS #
|
|
############################
|
|
|
|
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)))
|
|
return timeslots[0][0]
|
|
|
|
|
|
def get_last_on_day(day):
|
|
if day == 0:
|
|
return 4
|
|
else:
|
|
return (day + 1) * 5
|
|
|
|
|
|
def get_first_on_day(day):
|
|
if day == 3:
|
|
return 15
|
|
else:
|
|
return (day) * 5
|
|
|
|
|
|
for workgroup in workgroups:
|
|
if workgroup.constrainted_time:
|
|
for constrainted_time in workgroup.constrainted_time:
|
|
# TODO constraint for 2 slot workgroups missing!
|
|
timeslot_id = time_to_id(timeslots, constrainted_time['day'], constrainted_time['time'])
|
|
timeslot = timeslots[timeslot_id] # after this slot: ok
|
|
operator1 = '<' 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
|
|
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}.')
|
|
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 += "pool_schedule(ROOM) :- schedule(_,_,ROOM), pool(ROOM).\n"\
|
|
"poolpen(T) :- T = {pool_schedule(_)}.\n"\
|
|
"otherroomsametrack(AK1, AK2) :- ak(AK1,_, TRACK, _,_,_), schedule(AK1, _, ROOM1), ak(AK2,_, TRACK, _,_,_), schedule(AK2, _, ROOM2), ROOM1 != ROOM2.\n"\
|
|
"otherroomsametrackpen(T) :- T = {otherroomsametrack(_, _)}.\n"\
|
|
"finalpen(T) :- poolpen(P),otherroomsametrackpen(O), T = P+O.\n"\
|
|
"#minimize { T : finalpen(T) }.\n"\
|
|
"#show schedule/3."
|
|
|
|
#######################
|
|
# GENERATE SCHEDULE #
|
|
#######################
|
|
|
|
output_file_name = "generated_rules.pl"
|
|
|
|
open(output_file_name, 'w').write(rules)
|
|
|
|
# create subprocess definition
|
|
process = ['clingo', output_file_name, '--outf=2']
|
|
|
|
# run subprocess, not sure, if busy-waiting..
|
|
completed_process = subprocess.run(process, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL)
|
|
|
|
output = completed_process.stdout
|
|
|
|
open('solver_output.json', 'w').write(output)
|
|
|
|
#######################
|
|
# OUTPUT SCHEDULE #
|
|
#######################
|
|
|
|
if 'UNSATISFIABLE' in output:
|
|
print('UNSATISFIABLE')
|
|
print(output)
|
|
else:
|
|
print('SATISFIABLE, outputting schedule...')
|
|
import re
|
|
|
|
output = json.loads(output)
|
|
|
|
schedules = []
|
|
workgroup_to_schedule = defaultdict(list)
|
|
for i, schedule in enumerate(output['Call'][0]['Witnesses'][-1]['Value']):
|
|
match = re.match('schedule\((.+),"(.+)#(.+)#.+",(.+)\)', schedule)
|
|
try:
|
|
workgroup_index = id_to_index_workgroup[int(match.group(1))]
|
|
room_id = id_to_index_room[int(match.group(4))]
|
|
schedules.append(
|
|
Schedule(i, data['workGroups'][workgroup_index], match.group(2), match.group(3), data['rooms'][room_id]))
|
|
# {
|
|
# 'id': i,
|
|
# 'workGroup': data['workGroups'][workgroup_id],
|
|
# 'room': data['rooms'][room_id],
|
|
# 'time': match.group(3),
|
|
# 'day': match.group(2),
|
|
# 'lockRoom': False,
|
|
# 'lockTime': False,
|
|
# })
|
|
workgroup_to_schedule[workgroup_index].append(i)
|
|
except Exception as e:
|
|
print(e)
|
|
|
|
schedules_filtered = []
|
|
|
|
for workgroup_index in workgroup_to_schedule:
|
|
schedules_for_workgroup = workgroup_to_schedule[workgroup_index]
|
|
if len(schedules_for_workgroup) == 1:
|
|
schedules_filtered.append(schedules[schedules_for_workgroup[0]])
|
|
else:
|
|
# more than one schedule contains workgroup, because workgroup is 2 slots long
|
|
# find out which one is the first one and remove the second workgroup:
|
|
schedules_for_workgroup_0 = schedules[schedules_for_workgroup[0]]
|
|
schedules_for_workgroup_1 = schedules[schedules_for_workgroup[1]]
|
|
print(schedules_for_workgroup_0.time < schedules_for_workgroup_1.time)
|
|
print(f'{schedules_for_workgroup_0.time} < {schedules_for_workgroup_1.time}')
|
|
print(type(schedules_for_workgroup_0.time), type(schedules_for_workgroup_1.time))
|
|
print('-------')
|
|
if int(schedules_for_workgroup_0.time) < int(schedules_for_workgroup_1.time):
|
|
schedules_filtered.append(schedules_for_workgroup_0)
|
|
else:
|
|
schedules_filtered.append(schedules_for_workgroup_1)
|
|
|
|
data = {}
|
|
data['schedules'] = [s.to_dict() for s in schedules_filtered]
|
|
json.dump(data, open('output.json', 'w'))
|