constraint_adder.cpp

#include "constraint_adder.h"

#include <iostream>
#include <vector>
#include "clauses.h"
#include "constraint_encoder.h"
#include "core/SolverTypes.h"
#include "global.h"
#include "timetabler.h"
#include "utils.h"

using namespace NSPACE;

ConstraintAdder::ConstraintAdder(ConstraintEncoder *encoder,
                                 Timetabler *timetabler) {
  this->encoder = encoder;
  this->timetabler = timetabler;
}

Clauses ConstraintAdder::fieldSingleValueAtATime(FieldType fieldType) {
  Clauses result;
  result.clear();
  std::vector<Course> courses = timetabler->data.courses;
  for (unsigned i = 0; i < courses.size(); i++) {
    for (unsigned j = i + 1; j < courses.size(); j++) {
      /*
       * For every pair of courses, either the field value of the
       * FieldType is different or their times do not intersect
       */
      Clauses antecedent =
          encoder->hasSameFieldTypeNotSameValue(i, j, fieldType);
      Clauses consequent = encoder->notIntersectingTime(i, j);
      result.addClauses(antecedent | consequent);
    }
  }
  return result;
}

Clauses ConstraintAdder::instructorSingleCourseAtATime() {
  return fieldSingleValueAtATime(FieldType::instructor);
}

Clauses ConstraintAdder::classroomSingleCourseAtATime() {
  return fieldSingleValueAtATime(FieldType::classroom);
}

Clauses ConstraintAdder::programSingleCoreCourseAtATime() {
  Clauses result;
  result.clear();
  std::vector<Course> courses = timetabler->data.courses;
  for (unsigned i = 0; i < courses.size(); i++) {
    for (unsigned j = i + 1; j < courses.size(); j++) {
      /*
       * For every pair of courses, either there is no Program for which
       * they are both core or their times do not intersect
       */
      Clauses antecedent = encoder->hasNoCommonCoreProgram(i, j);
      Clauses consequent = encoder->notIntersectingTime(i, j);
      result.addClauses(antecedent | consequent);
    }
  }
  return result;
}

std::vector<Clauses> ConstraintAdder::minorInMinorTime() {
  std::vector<Course> courses = timetabler->data.courses;
  std::vector<Clauses> result(courses.size());
  for (unsigned i = 0; i < courses.size(); i++) {
    result[i].clear();
    /*
     * a minor course must be in a minor Slot.
     * a non-minor course must not be in a minor Slot.
     */
    Clauses antecedent = encoder->isMinorCourse(i);
    Clauses consequent = encoder->slotInMinorTime(i);
    result[i].addClauses(antecedent >> consequent);
    result[i].addClauses(consequent >> antecedent);
  }
  return result;
}

std::vector<Clauses> ConstraintAdder::exactlyOneFieldValuePerCourse(
    FieldType fieldType) {
  std::vector<Course> courses = timetabler->data.courses;
  std::vector<Clauses> result(courses.size());
  for (unsigned i = 0; i < courses.size(); i++) {
    result[i].clear();
    // exactly one field value must be true
    Clauses exactlyOneFieldValue =
        encoder->hasExactlyOneFieldValueTrue(i, fieldType);
    Clauses cclause(timetabler->data.highLevelVars[i][fieldType]);
    // high level variable implies the clause, and by default is hard
    // if high level variable is false, this clause could not be satisfied
    // this provides a reason to the user
    result[i].addClauses(cclause >> exactlyOneFieldValue);
  }
  return result;
}

void ConstraintAdder::addSingleConstraint(PredefinedClauses clauseType,
                                          const Clauses &clauses,
                                          const int course) {
  if (course == -1) {
    if (timetabler->data.predefinedClausesWeights[clauseType] != 0) {
      Clauses hardConsequent =
          CClause(timetabler->data.predefinedConstraintVars[clauseType][0]) >>
          clauses;
      timetabler->addClauses(hardConsequent, -1);
    }
    timetabler->addHighLevelConstraintClauses(clauseType, -1);
  } else {
    if (timetabler->data.predefinedClausesWeights[clauseType] != 0) {
      Clauses hardConsequent =
          CClause(
              timetabler->data.predefinedConstraintVars[clauseType][course]) >>
          clauses;
      timetabler->addClauses(hardConsequent, -1);
    }
    timetabler->addHighLevelConstraintClauses(clauseType, course);
  }
}

void ConstraintAdder::addConstraints() {
  std::vector<int> weights = timetabler->data.predefinedClausesWeights;
  // add the constraints to the formula
  addSingleConstraint(PredefinedClauses::instructorSingleCourseAtATime,
                      instructorSingleCourseAtATime(), -1);
  addSingleConstraint(PredefinedClauses::classroomSingleCourseAtATime,
                      classroomSingleCourseAtATime(), -1);
  addSingleConstraint(PredefinedClauses::programSingleCoreCourseAtATime,
                      programSingleCoreCourseAtATime(), -1);

  auto clauses = minorInMinorTime();
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::minorInMinorTime, clauses[i], i);
  }

  clauses = programAtMostOneOfCoreOrElective();
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::programAtMostOneOfCoreOrElective,
                        clauses[i], i);
  }

  clauses = exactlyOneFieldValuePerCourse(FieldType::slot);
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::exactlyOneSlotPerCourse, clauses[i],
                        i);
  }

  clauses = exactlyOneFieldValuePerCourse(FieldType::classroom);
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::exactlyOneClassroomPerCourse,
                        clauses[i], i);
  }

  clauses = exactlyOneFieldValuePerCourse(FieldType::instructor);
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::exactlyOneInstructorPerCourse,
                        clauses[i], i);
  }

  clauses = exactlyOneFieldValuePerCourse(FieldType::isMinor);
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::exactlyOneIsMinorPerCourse,
                        clauses[i], i);
  }

  clauses = exactlyOneFieldValuePerCourse(FieldType::segment);
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::exactlyOneSegmentPerCourse,
                        clauses[i], i);
  }

  clauses = coreInMorningTime();
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::coreInMorningTime, clauses[i], i);
  }

  clauses = electiveInNonMorningTime();
  for (unsigned i = 0; i < clauses.size(); i++) {
    addSingleConstraint(PredefinedClauses::electiveInNonMorningTime, clauses[i],
                        i);
  }
}

/*Clauses ConstraintAdder::softConstraints() {
    return existingAssignmentClausesSoft();
}*/

std::vector<Clauses> ConstraintAdder::coreInMorningTime() {
  std::vector<Course> courses = timetabler->data.courses;
  std::vector<Clauses> result(courses.size());
  for (unsigned i = 0; i < courses.size(); i++) {
    result[i].clear();
    Clauses coreCourse = encoder->isCoreCourse(i);
    Clauses morningTime = encoder->courseInMorningTime(i);
    result[i].addClauses(coreCourse >> morningTime);
  }
  return result;
}

std::vector<Clauses> ConstraintAdder::electiveInNonMorningTime() {
  std::vector<Course> courses = timetabler->data.courses;
  std::vector<Clauses> result(courses.size());
  for (unsigned i = 0; i < courses.size(); i++) {
    result[i].clear();
    Clauses coreCourse = encoder->isElectiveCourse(i);
    Clauses morningTime = encoder->courseInMorningTime(i);
    result[i].addClauses(coreCourse >> (~morningTime));
  }
  return result;
}

std::vector<Clauses> ConstraintAdder::programAtMostOneOfCoreOrElective() {
  std::vector<Course> courses = timetabler->data.courses;
  std::vector<Clauses> result(courses.size());
  for (unsigned i = 0; i < courses.size(); i++) {
    result[i].clear();
    result[i].addClauses(encoder->programAtMostOneOfCoreOrElective(i));
  }
  return result;
}