Generador d'horaris d'instituts

Abstract

Una de les majors complicacions que han de superar els instituts a l'hora d'organitzar el nou curs acadèmic és la confecció dels horaris. L'elevat nombre de combinacions entre assignatures difculta moltíssim el procés de confeccionar un horari viable i equitatiu. Amb l'aparició dels computadors, molts instituts van relegar aquesta feina a eines informàtiques capaces d'explorar centenars de milers de combinacions per segon. Tot i això, aquelles primeres eines no semblaven tenir millor fortuna ja que el nombre de combinacions possibles rere un problema d'aquestes característiques és exponencial al nombre d'assignatures. Per tant, també es tenien moltíssimes dificultats per generar horaris viables. Aquests horaris generalment eren de baixa qualitat i requerien d'un refinament manual posterior. Un altre aspecte que afegeix complexitat al problema és la gran varietat de requeriments dels horaris, que varien d'un país a un altre. En particular dificulta l'abstracció necessària a l'hora de modelar una eina capaç de generar horaris de manera satisfactòria per instituts d'arreu. Aquest fet fa difícil la creació de generadors capaços d'explotar les peculiaritats inherents a cada instància concreta. Encara avui dia, no es coneix cap eina capaç de resoldre el problema de manera determinista i en un temps raonable. Però l'estat de l'art ha avançat moltíssim i ja són pocs els instituts que opten per atacar el problema de manera manual. Els objectius d'aquest treball són per una banda, aprofundir sobre el problema de la confecció d'horaris, veure com de dur és el problema, què és el que el fa tan dur i aprofundir en les tècniques deterministes de més èxit a l'actualitat. I per altra banda, implementar un generador determinista capaç de generar horaris per a instàncies de formulació específica utilitzant dues de les tecnologies amb més èxit i futur en el sí de l'estat de l'art actual, com són tècniques basades en SAT (Satisfactibilitat proposicional booleana) i tècniques basades en SMT (Satisfiability Modulo Theories)