Timetabler
|
Class for constraint encoder. More...
#include <constraint_encoder.h>
Public Member Functions | |
ConstraintEncoder (Timetabler *) | |
Constructs the ConstraintEncoder object. More... | |
Clauses | hasSameFieldTypeAndValue (int, int, FieldType) |
Gives Clauses that represent that a pair of courses have the same field value for a given FieldType. More... | |
Clauses | hasSameFieldTypeNotSameValue (int, int, FieldType) |
Gives Clauses that represent that a pair of courses do not have the same field value for a given FieldType. More... | |
Clauses | notIntersectingTime (int, int) |
Gives Clauses that represent that a pair of courses cannot have an intersecting schedule. More... | |
Clauses | notIntersectingTimeField (int, int, FieldType) |
Gives Clauses that represent that a pair of courses cannot have an intersecting value for a given FieldType, where the FieldType is of a time field, which is either a Segment or a Slot. More... | |
Clauses | hasExactlyOneFieldValueTrue (int, FieldType) |
Gives Clauses that represent that a Course can have exactly one field value of a given FieldType to be True. More... | |
Clauses | hasAtLeastOneFieldValueTrue (int, FieldType) |
Gives Clauses that represent that a Course can have at least one field value of a given FieldType to be True. More... | |
Clauses | hasAtMostOneFieldValueTrue (int, FieldType) |
Gives Clauses that represent that a Course can have at most one field value of a given FieldType to be True. More... | |
Clauses | hasCommonProgram (int, int) |
Gives Clauses that represent that a pair of courses are core for a given Program. More... | |
Clauses | hasNoCommonCoreProgram (int, int) |
Gives Clauses that represent that at least one out of a pair of courses is not core for a given Program. More... | |
Clauses | isMinorCourse (int) |
Gives Clauses that represent that a given Course is a minor Course. More... | |
Clauses | slotInMinorTime (int) |
Gives Clauses that represent that a given Course must have a minor Slot. More... | |
Clauses | isCoreCourse (int) |
Gives Clauses that represent that a Course is a core Course. More... | |
Clauses | isElectiveCourse (int) |
Gives Clauses that represent that a Course is an elective Course. More... | |
Clauses | courseInMorningTime (int) |
Gives Clauses that represent that a Course is scheduled in a morning Slot. More... | |
Clauses | programAtMostOneOfCoreOrElective (int) |
Gives Clauses that represent that for a Course, it can be a part of a Program as at most one out of core or elective. More... | |
Clauses | hasFieldTypeListedValues (int, FieldType, std::vector< int >) |
Gives Clauses that represent that a Course has a field value for a given FieldType out of a list of possible values. More... | |
Class for constraint encoder.
This class is responsible for imposing constraints given a Course or a pair of Courses and a FieldType. The constraints are of a higher level than the operations of Clauses and of a lower level than the constraints defined in ConstraintAdder, which are the final constraints added to the solver. The class keeps a copy of the variables used for every 3-tuple of (Course, FieldType, field value) and a pointer to a Timetabler object to access the field data. Clauses for these constraints are created using the operations defined in Clauses.
Definition at line 26 of file constraint_encoder.h.
ConstraintEncoder::ConstraintEncoder | ( | Timetabler * | timetabler | ) |
Constructs the ConstraintEncoder object.
timetabler | The time tabler |
Definition at line 19 of file constraint_encoder.cpp.
References Timetabler::data, Data::fieldValueVars, and timetabler.
Clauses ConstraintEncoder::courseInMorningTime | ( | int | course | ) |
Gives Clauses that represent that a Course can have at least one field value of a given FieldType to be True.
[in] | course | The course |
[in] | fieldType | The field type |
Definition at line 215 of file constraint_encoder.cpp.
References CClause::createLitAndAdd().
Gives Clauses that represent that a Course can have at most one field value of a given FieldType to be True.
The binomial encoding has been used to represent this constraint. A more efficient encoding, with auxiliary variables, has not been used because such an encoding would only be equisatisfiable. However, when using these clauses as an antecedent of an implication, we need that if the antecedent of the encoded clauses is False, the original set of clauses would also have been False, a property that equisatifiability does not guarantee.
[in] | course | The course |
[in] | fieldType | The field type |
Definition at line 242 of file constraint_encoder.cpp.
References Clauses::addClauses().
Clauses ConstraintEncoder::hasCommonProgram | ( | int | course1, |
int | course2 | ||
) |
Gives Clauses that represent that a pair of courses are core for a given Program.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
Definition at line 90 of file constraint_encoder.cpp.
Gives Clauses that represent that a Course can have exactly one field value of a given FieldType to be True.
This is helpful for defining constraints such as that that a given Course must have exactly one Instructor.
[in] | course | The course |
[in] | fieldType | The field type |
Definition at line 199 of file constraint_encoder.cpp.
Clauses ConstraintEncoder::hasFieldTypeListedValues | ( | int | course, |
FieldType | fieldType, | ||
std::vector< int > | indexList | ||
) |
Gives Clauses that represent that a Course has a field value for a given FieldType out of a list of possible values.
This is useful for encoding custom constraints.
[in] | course | The course |
[in] | fieldType | The field type |
[in] | indexList | A vector of indices of the data corresponding to the FieldType for the allowed field values of the type. |
Definition at line 410 of file constraint_encoder.cpp.
References CClause::createLitAndAdd().
Clauses ConstraintEncoder::hasNoCommonCoreProgram | ( | int | course1, |
int | course2 | ||
) |
Gives Clauses that represent that at least one out of a pair of courses is not core for a given Program.
This is helpful to represent that two courses that are core for a Program cannot have an intersecting schedule.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
Definition at line 119 of file constraint_encoder.cpp.
Clauses ConstraintEncoder::hasSameFieldTypeAndValue | ( | int | course1, |
int | course2, | ||
FieldType | fieldType | ||
) |
Gives Clauses that represent that a pair of courses have the same field value for a given FieldType.
For example, it can be used to represent that two courses have the same Slot. This is helpful for constructing constraints such as those enforcing that two courses have the same Slot.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
[in] | fieldType | The field type |
Definition at line 38 of file constraint_encoder.cpp.
References CClause::createLitAndAdd().
Clauses ConstraintEncoder::hasSameFieldTypeNotSameValue | ( | int | course1, |
int | course2, | ||
FieldType | fieldType | ||
) |
Gives Clauses that represent that a pair of courses do not have the same field value for a given FieldType.
For example, it can be used to represent that two courses do not have the same Instructor. This is helpful to define constraints such as that that an Instructor cannot have two courses at the same time.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
[in] | fieldType | The field type |
Definition at line 68 of file constraint_encoder.cpp.
References Clauses::addClauses(), and CClause::addLits().
Clauses ConstraintEncoder::isCoreCourse | ( | int | course | ) |
Clauses ConstraintEncoder::isElectiveCourse | ( | int | course | ) |
Clauses ConstraintEncoder::isMinorCourse | ( | int | course | ) |
Clauses ConstraintEncoder::notIntersectingTime | ( | int | course1, |
int | course2 | ||
) |
Gives Clauses that represent that a pair of courses cannot have an intersecting schedule.
This describes that either the pair of courses have slots that do not intersect or that they have segments that do not intersect.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
Definition at line 144 of file constraint_encoder.cpp.
Clauses ConstraintEncoder::notIntersectingTimeField | ( | int | course1, |
int | course2, | ||
FieldType | fieldType | ||
) |
Gives Clauses that represent that a pair of courses cannot have an intersecting value for a given FieldType, where the FieldType is of a time field, which is either a Segment or a Slot.
[in] | course1 | The course 1 |
[in] | course2 | The course 2 |
[in] | fieldType | The field type |
Definition at line 163 of file constraint_encoder.cpp.
Clauses ConstraintEncoder::programAtMostOneOfCoreOrElective | ( | int | course | ) |
Clauses ConstraintEncoder::slotInMinorTime | ( | int | course | ) |