В данном репозитории приводятся исходный код к програмному решению, реализованному в рамках дипломной работы.

Програмное решение выполняет решение задачи автоматического составления расписания занятий в университете для заданного списка учебных групп с помощью SMT солвера. Более подробное описание дипломной работы можно найти в расчетно пояснительной записке. Данное решение соститоит из базы данных, в которой хранится вспомогательная информация для составления расписания, а также из ряда утилит для генерации расписания и формирования pdf-документа с раписанием занятий группы.

Проект реализован на языке Java. Для сбоорки проекта использовался Maven. Весь проект состоит из следующих модулей (каждому модулю соответствует одноименная папка в корневой директории проекта):

• dbfill - консольная утилита для заполения базы;
• smtgen - косольная утилита для автоматического составления расписания с помощью SMT-солвера.
• pdfgen - консольная утилита для генерации pdf-документа для заданной группы.
• schedule-core - вспомогательны модуль, содержит базовые классы, необходимые для решения вышеописанных утилит: классы-сущности базы, репозитории для доступа к данным, файл конфигурации настройки Hibernate (параметры подключения, стратегия обновления сущностей, список сущностей) и др.
• schedule-parser - вспомогательный модуль, содержит классы для парсинга csv-файлов, а также парсинга html-страниц с расписанием. Парсинг html-страниц используется для сбора вспомогательной информации, которая нужна на этапе составления расписания. Парсинг csv-файлов используется для заполнения базы данными с помощью утилиты dbfill.

По-мимо папки с модулями, в данном репозитории можно найти следующие директории:

• ./build - готовые jar-приложения (утилита smtgen может не работать на разных архитектурах из-за библиотеки Z3, поэтому может понадобиться пересборка данного модуля).
• ./docs - папка с вспомогательными материалами (документами), которые использовались входе выполнения ВКР.
• ./sql - скрипты для создания базы.

Для запуска утилит понадобиться JRE 1.8, и PostgreSQL версии 10.8, либо docker в зависимости от выбранного способа установки и настройки базы.

Данный пункт является обязательным, поскольку большинство утилит используют базу данных для хранения вспомогательных данных, которые необходимы для составления расписания.

Для установки и настройки базы можно воспользоваться одним из следующих вариантов:

а) накатить docker-контейнер с базой:

1. Скачиваем docker-образ:

$ docker pull karkinai/schedule-db

Для выполнения данной команды понадобиться установить Docker. Для запуска в ОС Linux Ubuntu необходимо установить Docker CE. Для запуска команды на Windows понадобиться установить Docker Toolbox для Windows. Если на компьютере установлена ОС Windows 10 Pro, то вместо Docker Toolbox можно поставить Docker Desktop.

2. Запускаем контейнер с базой:

$ docker run --rm -p 5432:5432 --name scheduledb karkinai/schedule-db

Замечания:

1. Для запуска контейнера в режиме демона, можно доабавить ключ -d
2. Для того, чтобы данные не стирались при каждом запуске, можно смонтировать папку с данными PostgreSQL в локальную папку. Для этого нужно добавить параметр -v при запуске:
   -v {путь к локальной папке, где будут хранится данные}:/var/lib/postgresql/pgdata.

б) установить Postgres локально, после чего прогнать скрипты создания и заполненить базу тестовыми данными с помощью утилиты dbfill:

На ОС Linux Ubuntu для установки и настройки postgres потребуется выполнить следующие шаги.

1. Установить Postgres с помощью следующей команды в терминале:

$ sudo apt-get install postgresql postgresql-contrib

2. Затем, создать пользователя в базе (рекомендуемое имя пользователя и пароль "admin"):

$ sudo -u postgres createuser admin
$ sudo -u postgres psql
psql=# alter user admin with encrypted password 'admin';

3. Запустить скрипт для создания таблиц базы данных:

$ psql --username postgres --dbname postgres -a -f ./sql/init.sql

4. Заполнить базу тестовыми данными, выполнив команду

$ java -jar ./build/dbfill.jar ./dbfill/src/main/resources/config.properties

Если при создании пользователя в postgres указывались реквизиты, отличные от приведенных в примере, то необходимо поменять параметры базы в файле ./schedule-core/src/main/resources/hibernate.cfg.xml на реквизиты пользователя указанные в пункте 2:

<?xml version='1.0' encoding='utf-8'?>
<!DOCTYPE hibernate-configuration PUBLIC
        "-//Hibernate/Hibernate Configuration DTD//EN"
        "http://www.hibernate.org/dtd/hibernate-configuration-3.0.dtd">

<hibernate-configuration>
    <session-factory>

        <property name="connection.driver_class">org.postgresql.Driver</property>
        <property name="connection.url">jdbc:postgresql://{хост подключения к базе}:{порт подключения}/bmstu_schedule</property>
        <property name="connection.username">{имя пользователя, указанное в пункет 2}</property>
        <property name="connection.password">{пароль, указанный в пункет 2}</property>
        ...
    </session-factory>
</hibernate-configuration>

После этого необходимо пересобрать модуль dbfill ( о том как это сделать говорится в следующем разделе), после чего в директории модуля выполнить команду:

$ java -jar ./target/dbfill.jar

Для сборки всего проекта понадобиться установить следующее:

1. JDK 1.8 (обязательно)
2. Python 2.7 (для сборки smtgen)
3. Библиотеку Z3 и байндинги для Java (для сборки smtgen)
4. Apache Maven v3.6+ (обязательно)
5. Git (для сборки smtgen)

Для сборки данной утилиты необходимо сначала скачать байндинги библиотеки Z3 для Java.

Библиотека Z3, а также байндинг для языка Java предоставляются уже в собранном виде под большинство ОС рерозитории Z3.

Однако, в случае если утилита smtlib запускается на нестандартной ОС или на нестандартной архитектуре, библиотеку Z3 и API для Java можно пересобрать, выполнив следующие действия.

1. Склонировать репозиторий с Z3 на локальный компьютер, выполнив команду в терминале:

$ cd {папка, где будет располагаться z3}
$ git clone https://github.com/Z3Prover/z3.git

2. Собрать Z3 и байндинги для Java, выполнив команду в терминале в той же директории:

$ python scripts/mk_make.py –-java
$ cd ./build && make
$ sudo make install

После того, как библиотека Z3 и байндинг данной библиотеки для Java собран, перед переходом к процедуре сборки утилиты smtgen необходимо установить API для Java в локальном Maven репозитории. Для этого в директории с библиотекой Z3 (там где располагается файл com.microsoft.z3.jar) неообходимо выполнить команду в командной строке:

$ mvn instal:install-file -Dfile=com.microsoft.z3.jar 
-DgroupId=com.microsoft.z3 -DartifactId=javasmt-solver-z3 
-Dversion=4.8.4 -Dpackaging=jar

Для сборки всего проекта необходимо перейти в директорию с проектом и выполнить команду для сборки:

$ cd {корневая директория проекта}
$ mvn clean install -DskipTests=true

После выполнения в каждой папке Maven-модуля данного проекта, появиться папка ./target, в которой располагается исполняемый файл каждой из утилит для JVM (точнее, JAR-архив). О том как запустить, каждое приложение говорится в следующем разделе.

Для сборки отедльного модуля, достаточно перейти в директорию модуля и выполнить ту же команду:

$ cd {корневая директория проекта}/{название модуля}
$ mvn clean install -DskipTests=true

В случае, если приведенные ниже утилиты запускаются на ОС Windows русские символы могут некорректно оторбражаться в консоли. Поэтому при запуске утилит из командной строки, командную строку (cmd.exe) следует запускать с ключом chcp 1251, для этого: зажать сочетание клавиш WK+R (открыть окно "выполнить") и в появившемся окне прописать строчку:

cmd /K chcp 1251

При запуск утилит из-под Windows в командной строке могут также некорректно считываться аргументы командной строки, поэтому для успешной работы с утилитами при запуске, необходимо добавить JVM параметр sun.jnu.encoding=UTF-8. Например:

java -Dsun.jnu.encoding=UTF-8 -jar pdfgen.jar . ИУ9-21

Данная утилита выполняет заполнение базы. В качестве аргумента командной строки в данную утилиту передается путь к конфигурационному .properties-файлу. В этом файле прописываются пути к csv-справочникам, которые используются для заполения таблиц базы.

Для демонстрации работы программы использулся конфигурационный файл - config.properties. В данном файле приводятся пути к csv-справочникам, содержащими данные для кафедры ИУ9. Этот же файл используется для заполнения базы данными при первом запуске docker-контейнера (см. раздел Установка и настройка базы, пункт а).

Результатом успешного завершения данной утилиты будет заполненная база данных.

Утилита выполняет автоматическое составление раписания. На вход данная утилита принимает, в качестве, аргументов командной строки одно из двух:

а) список шифров групп перечисленных через запятую (ключ -g);

б) информацию об учебном плане учебного потока: код специализации (ключ -s), код кафедры (ключ -d), год начала обучения учебных групп (ключ -y), номер текущего семестра данных групп (ключ -t).

Если указываются ключ из пункта а), все ключи пункта б) игнорируются. Если не указывается ключ -g, то должны быть указаны все ключи перечисленные в пункте б). В противном случае программа выдаст сообщение об ошибке.

Примеры запуска программы (из директории с приложением):

$ java -jar smtgen.jar -g ИУ9-21, ИУ9-22

или

$ java -jar smtgen.jar -y 2018 -t 2 -s 01.03.02_1 -d ИУ9

Результат работы программы - сохранение расписания для заданного списка групп в базу.

Результат успешного выполнения данной программы демонстрирует утилита pdfgen, описание которой приводится в следующем разделе.

Для всего учебного потока программа будет работать медленно, либо может вообще не завершится. Данное обстоятельство связано не с "кривой" реализацией дипломного проекта, а с особенностью поставленной задачей, которая относится к классу NP-полных. SMT-солвер (Z3) зацикливается при постановки такого рода задач для большого числа ограничений (проверено научным руководителем). Об этом же говорится в пояснительной записке. Рекомендуется запускать утилиту smtgen с числом групп не более 3 (больше 4 можно не даждаться, больше 5 - солвер может зациклиться или выдать некорректный результат). Оптимально: 1-2 группы, занимает максимум минут 10 (тестировал на своем ноутбуке: процессор - Intel Core i3, 1.9GHz x 4, память: 4Gb)

Полный список ключей утилиты:

-h, --help 
-g, --groups <Список шифров учебных групп>
-d, --dept <Шифр кафедры>
-s, --spec <Код специализации>
-y, --year <Год начала обучения, соотвествует году учебном плане>
-t, --term <Номер семестра>

Данная утилита генерирует pdf-документ с раписанием занятий учебной группы.

Если учебное группа или расписание занятий для данной группы отсутвует в базе, то программа выдает сообщение об ошибке.

Программа, в качестве входных параметров, принимает следующие аргументы командной строки в заданном порядке:

1. путь к папке, где будет располагаться pdf-файл с расписанием учебной группы;

2. шифр учебной группы, для которой необходимо составить расписание.

В результате успешного завершения программа должна сохранить pdf-документ с расписанием в указанную папку. Формат выходного файла соответствует шаблону: {шифр группы}.pdf. Если файл, с таким именем уже существует в указанной папке, то старый файл перезаписывается новым.

Пример запуска утилиты (из директории с приложением):

$ java -jar pdfgen.jar . ИУ9-21

Примеры результатов выполнения утилиты pdfgen приведены в папке examples.