diff --git a/.gitignore b/.gitignore index c26cfff..dc53b53 100644 --- a/.gitignore +++ b/.gitignore @@ -40,9 +40,16 @@ dependencies *.swp +# Version +include/version.h +TimetablerVersion.cmake + # Snap *.snap +snap/.snapcraft *.xdelta* parts prime stage +.idea +cmake-build-debug diff --git a/CMakeLists.txt b/CMakeLists.txt index b1c4e6b..26ab97e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,13 +6,13 @@ include(TimetablerVersion.cmake) set(CMAKE_BUILD_TYPE Release CACHE STRING "Build type") -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wno-parentheses -Wno-misleading-indentation") +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wno-parentheses -Wno-misleading-indentation -Wpedantic") set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -DTIMETABLERDEBUG") set(OPEN_WBO_PATH "${CMAKE_SOURCE_DIR}/dependencies/open-wbo" CACHE PATH "Open-WBO path") -set(YAML_CPP_PATH "${CMAKE_SOURCE_DIR}/dependencies/yaml-cpp-yaml-cpp-0.6.2" CACHE PATH "YAML CPP path") +set(YAML_CPP_PATH "${CMAKE_SOURCE_DIR}/dependencies/yaml-cpp" CACHE PATH "YAML CPP path") set(CSVPARSER_PATH "${CMAKE_SOURCE_DIR}/dependencies/CSVparser" CACHE PATH "CSVParser path") -set(PEGTL_PATH "${CMAKE_SOURCE_DIR}/dependencies/PEGTL-2.7.0" CACHE PATH "PEGTL path") +set(PEGTL_PATH "${CMAKE_SOURCE_DIR}/dependencies/PEGTL" CACHE PATH "PEGTL path") set(ENABLE_TESTS "OFF" CACHE BOOL "Enable Google tests") set(GTEST_PATH "${CMAKE_SOURCE_DIR}/dependencies/googletest-release-1.8.1" CACHE PATH "GTest path") diff --git a/TimetablerVersion.cmake b/TimetablerVersion.cmake deleted file mode 100644 index 2ccfc16..0000000 --- a/TimetablerVersion.cmake +++ /dev/null @@ -1,6 +0,0 @@ -set(Timetabler_VERSION_MAJOR 0) -set(Timetabler_VERSION_MINOR 3) -set(Timetabler_VERSION_PATCH 0) -# Set to "" for tagged release and "+git" for others -set(Timetabler_VERSION_SUFFIX "+git") -set(Timetabler_VERSION ${Timetabler_VERSION_MAJOR}.${Timetabler_VERSION_MINOR}.${Timetabler_VERSION_PATCH}${Timetabler_VERSION_SUFFIX}) diff --git a/docs/Doxyfile b/docs/Doxyfile index ae2a902..bf71e3b 100644 --- a/docs/Doxyfile +++ b/docs/Doxyfile @@ -1,11 +1,15 @@ PROJECT_NAME = "Timetabler" OUTPUT_DIRECTORY = build -INPUT = .. README.md -EXCLUDE = ../tests ../src/custom_parser.cpp +INPUT = .. ../README.md +EXCLUDE = ../tests ../dependencies ../snap ../parts ../prime ../stage ../build ../docs RECURSIVE = YES QUIET = YES GENERATE_HTML = YES GENERATE_XML = NO GENERATE_LATEX = NO -USE_MDFILE_AS_MAINPAGE = README.md +SOURCE_BROWSER = YES +REFERENCED_BY_RELATION = YES +REFERENCES_RELATION = YES +REFERENCES_LINK_SOURCE = YES +USE_MDFILE_AS_MAINPAGE = ../README.md diff --git a/gen_version.sh b/gen_version.sh new file mode 100755 index 0000000..ca7e3f4 --- /dev/null +++ b/gen_version.sh @@ -0,0 +1,15 @@ +#!/bin/bash +Timetabler_VERSION=$(git describe --always --tags) +if [ -z "$Timetabler_VERSION" ] +then + # Update the below line after every release + Timetabler_VERSION="v0.3.0" +fi +VERSION_INCLUDE_STR="#ifndef __TIMETABLER_VERSION__\n#define __TIMETABLER_VERSION__ \"${Timetabler_VERSION}\"\n#endif" +if [ "$2" == "1" ] +then + echo ${Timetabler_VERSION:1} +else + echo -e $VERSION_INCLUDE_STR > $1/include/version.h + echo "set (Timetabler_VERSION \"${Timetabler_VERSION:1}\")" > $1/TimetablerVersion.cmake +fi diff --git a/include/clauses.h b/include/clauses.h index d95a273..f9939ae 100644 --- a/include/clauses.h +++ b/include/clauses.h @@ -29,6 +29,7 @@ class Clauses { public: Clauses(const std::vector &); + Clauses(const vec &); Clauses(const CClause &); Clauses(const Lit &); Clauses(const Var &); diff --git a/include/constraint_adder.h b/include/constraint_adder.h index 68bf304..663bf30 100644 --- a/include/constraint_adder.h +++ b/include/constraint_adder.h @@ -36,20 +36,21 @@ class ConstraintAdder { */ Timetabler *timetabler; Clauses fieldSingleValueAtATime(FieldType); - Clauses exactlyOneFieldValuePerCourse(FieldType); + std::vector exactlyOneFieldValuePerCourse(FieldType); Clauses instructorSingleCourseAtATime(); Clauses classroomSingleCourseAtATime(); Clauses programSingleCoreCourseAtATime(); - Clauses minorInMinorTime(); - Clauses coreInMorningTime(); - Clauses electiveInNonMorningTime(); - Clauses existingAssignmentClauses(); - Clauses programAtMostOneOfCoreOrElective(); + std::vector minorInMinorTime(); + std::vector coreInMorningTime(); + std::vector electiveInNonMorningTime(); + // Clauses existingAssignmentClauses(); + std::vector programAtMostOneOfCoreOrElective(); public: ConstraintAdder(ConstraintEncoder *, Timetabler *); void addConstraints(); - void addSingleConstraint(PredefinedClauses, const Clauses &); + void addSingleConstraint(PredefinedClauses, const Clauses &, + const int course); }; #endif diff --git a/include/custom_parser.h b/include/custom_parser.h index 2adc4f4..8bf83fa 100644 --- a/include/custom_parser.h +++ b/include/custom_parser.h @@ -52,14 +52,6 @@ struct Object { Object(); }; -/** - * @brief Parses custom constraints given in a file and adds them to the - * solver. - * - * @param[in] file The file containing the constraints - * @param constraintEncoder The ConstraintEncoder object - * @param timetabler The Timetabler object - */ void parseCustomConstraints(std::string file, ConstraintEncoder *constraintEncoder, Timetabler *timetabler); diff --git a/include/data.h b/include/data.h index efb7e8f..0dbb39d 100644 --- a/include/data.h +++ b/include/data.h @@ -3,6 +3,7 @@ #ifndef DATA_H #define DATA_H +#include #include #include #include "core/Solver.h" @@ -78,7 +79,13 @@ class Data { * can make the necessary changes. */ std::vector> highLevelVars; - std::vector predefinedConstraintVars; + /** + * Stores the high level variables associated with the predefined constraints. + */ + std::vector> predefinedConstraintVars; + /** + * Stores the high level variables associated with the custom constraints. + */ std::vector customConstraintVars; /** * Stores the existing assignments for every Course and @@ -115,6 +122,10 @@ class Data { * or to disable certain constraints. */ std::vector predefinedClausesWeights; + /** + * Stores the course with the associated custom constraint. + */ + std::map customMap; Data(); }; diff --git a/include/fields/course.h b/include/fields/course.h index 846a07a..44aade8 100644 --- a/include/fields/course.h +++ b/include/fields/course.h @@ -46,15 +46,15 @@ class Course { * the index of the type in the list of possible isMinor * values. */ - int isMinor; + MinorType isMinor; int classroom = -1; int slot = -1; public: - Course(std::string, unsigned, int, int, int); - Course(std::string, unsigned, int, int, int, std::vector); + Course(std::string, unsigned, int, int, MinorType); + Course(std::string, unsigned, int, int, MinorType, std::vector); void setPrograms(std::vector); void addProgram(int); void addClassroom(int); @@ -64,7 +64,7 @@ class Course { int getInstructor(); std::vector getPrograms(); int getSegment(); - int getIsMinor(); + MinorType getIsMinor(); int getClassroom(); int getSlot(); unsigned getClassSize(); diff --git a/include/fields/is_minor.h b/include/fields/is_minor.h index 3bb082a..02e0b09 100644 --- a/include/fields/is_minor.h +++ b/include/fields/is_minor.h @@ -13,7 +13,7 @@ * value under this enum would be isMinorCourse, and otherwise, * it would be isNotMinorCourse. */ -enum MinorType { +enum class MinorType { /** * Value when the Course is a minor course */ diff --git a/include/global.h b/include/global.h index 70ce728..c89e9a2 100644 --- a/include/global.h +++ b/include/global.h @@ -12,9 +12,9 @@ enum FieldType { instructor, segment, isMinor, program, classroom, slot }; * @brief Enum that represents all the predefined constraints. */ enum PredefinedClauses { - instructorSingleCourseAtATime, - classroomSingleCourseAtATime, - programSingleCoreCourseAtATime, + instructorSingleCourseAtATime, // 1 + classroomSingleCourseAtATime, // 1 + programSingleCoreCourseAtATime, // 1 minorInMinorTime, exactlyOneSlotPerCourse, exactlyOneInstructorPerCourse, diff --git a/include/global_vars.h b/include/global_vars.h index 43c28b8..8b45252 100644 --- a/include/global_vars.h +++ b/include/global_vars.h @@ -1,8 +1,13 @@ +/** @file */ + #ifndef GLOBAL_VARS_H #define GLOBAL_VARS_H #include "timetabler.h" +/** + * Timetabler variable + */ extern Timetabler *timetabler; #endif diff --git a/include/timetabler.h b/include/timetabler.h index ee06b95..b223873 100644 --- a/include/timetabler.h +++ b/include/timetabler.h @@ -9,6 +9,7 @@ #include "core/SolverTypes.h" #include "data.h" #include "mtl/Vec.h" +#include "totalizer.h" #include "tsolver.h" using namespace NSPACE; @@ -66,6 +67,7 @@ class Timetabler { void addClauses(const std::vector &, int); void addClauses(const Clauses &, int); bool checkAllTrue(const std::vector &); + bool checkAllTrue(const std::vector> &); bool isVarTrue(const Var &); SolverStatus solve(); Var newVar(); @@ -74,13 +76,15 @@ class Timetabler { void displayTimeTable(); void displayUnsatisfiedOutputReasons(); void addHighLevelClauses(); - void addHighLevelConstraintClauses(PredefinedClauses); + void addHighLevelConstraintClauses(PredefinedClauses, const int course); void addHighLevelCustomConstraintClauses(int, int); void writeOutput(std::string); void addExistingAssignments(); void addToFormula(vec &, int); void addToFormula(Lit, int); void displayChangesInGivenAssignment(); + Clauses generateAtMostKTotalizerEncoding(const std::vector &, + int64_t rhs = 1); }; #endif diff --git a/include/totalizer.h b/include/totalizer.h new file mode 100644 index 0000000..773eca9 --- /dev/null +++ b/include/totalizer.h @@ -0,0 +1,120 @@ +/*! + * \author Ruben Martins - ruben@sat.inesc-id.pt + * + * @section LICENSE + * + * Open-WBO, Copyright (c) 2013-2017, Ruben Martins, Vasco Manquinho, Ines Lynce + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + */ + +#ifndef Totalizer_h +#define Totalizer_h + +#include "MaxSATFormula.h" +#include "core/Solver.h" +#include "core/SolverTypes.h" +#include "mtl/Vec.h" + +using namespace openwbo; +using namespace NSPACE; + +class TTotalizer { + + public: + TTotalizer(int strategy = _INCREMENTAL_NONE_) { + blocking = lit_Undef; + hasEncoding = false; + joinMode = false; + current_cardinality_rhs = -1; // -1 corresponds to an unitialized value + incremental_strategy = strategy; + + n_clauses = 0; + n_variables = 0; + } + ~TTotalizer() {} + + void build(MaxSATFormula *formula, vec &lits, int64_t rhs); + void join(MaxSATFormula *formula, vec &lits, int64_t rhs); + void update(MaxSATFormula *formula, int64_t rhs, vec &lits, + vec &assumptions); + void update(MaxSATFormula *formula, int64_t rhs) { + vec lits; + vec assumptions; + update(formula, rhs, lits, assumptions); + } + + bool hasCreatedEncoding() { return hasEncoding; } + void setIncremental(int incremental) { incremental_strategy = incremental; } + int getIncremental() { return incremental_strategy; } + + int getNbClauses() { return n_clauses; } + int getNbVariables() { return n_variables; } + void resetCounters() { + n_clauses = 0; + n_variables = 0; + } + + vec &lits() { return ilits; } + vec &outputs() { return cardinality_outlits; } + + void addUnitClause(MaxSATFormula *formula, Lit a); + void addBinaryClause(MaxSATFormula *formula, Lit a, Lit b); + void addTernaryClause(MaxSATFormula *formula, Lit a, Lit b, Lit c); + + void newSATVariable(MaxSATFormula *formula); + + protected: + void encode(MaxSATFormula *formula, vec &lits); + void adder(MaxSATFormula *formula, vec &left, vec &right, + vec &output); + void incremental(MaxSATFormula *formula, int64_t rhs); + void toCNF(MaxSATFormula *formula, vec &lits); + + vec> totalizerIterative_left; + vec> totalizerIterative_right; + vec> totalizerIterative_output; + vec totalizerIterative_rhs; + + Lit blocking; // Controls the blocking literal for the incremental blocking. + bool hasEncoding; + + // TEMP + vec ilits; + vec olits; + + vec + cardinality_inlits; // Stores the inputs of the cardinality + // constraint encoding for the totalizer encoding + vec cardinality_outlits; // Stores the outputs of the cardinality + // constraint encoding for incremental solving + + int incremental_strategy; + int64_t current_cardinality_rhs; + + vec + disable_lits; // Contains a vector with a list of blocking literals. + bool joinMode; + + int n_clauses; + int n_variables; +}; + +#endif diff --git a/include/tsolver.h b/include/tsolver.h index 86e1aaa..3b20f1e 100644 --- a/include/tsolver.h +++ b/include/tsolver.h @@ -23,10 +23,14 @@ using namespace openwbo; * terminates, it simply returns. */ class TSolver : public OLL { - public: - TSolver(int verb = _VERBOSITY_MINIMAL_, int enc = _CARD_TOTALIZER_); - std::vector tSearch(); - void tWeighted(); + public: + TSolver(int, int); + std::vector tSearch(); + void tWeighted(); + // void encodeAtMostK(vec &lits, vec &assumptions, int64_t rhs = + // 1); + Var newVar(); + Lit newLiteral(bool sign = false); }; #endif diff --git a/include/version.h b/include/version.h deleted file mode 100644 index f19ec75..0000000 --- a/include/version.h +++ /dev/null @@ -1,3 +0,0 @@ -#ifndef __TIMETABLER_VERSION__ -#define __TIMETABLER_VERSION__ "0.3.0+git" -#endif diff --git a/install_dependencies.sh b/install_dependencies.sh index f66536a..2392210 100755 --- a/install_dependencies.sh +++ b/install_dependencies.sh @@ -31,6 +31,9 @@ if [ "$PARALLEL" = "-j" ] ; then echo "Running make jobs in parallel" fi +echo "Generating version files..." +./gen_version.sh . + mkdir -p dependencies cd dependencies @@ -45,16 +48,17 @@ LIB=open-wbo make libr $PARALLEL cd .. echo "Getting YAML-CPP..." -if [ ! -d yaml-cpp-yaml-cpp-$YAML_CPP_VERSION ] ; then +if [ ! -d yaml-cpp ] ; then wget -O yaml-cpp.tar.gz https://github.com/jbeder/yaml-cpp/archive/yaml-cpp-$YAML_CPP_VERSION.tar.gz tar -xf yaml-cpp.tar.gz rm yaml-cpp.tar.gz + mv yaml-cpp-yaml-cpp-$YAML_CPP_VERSION yaml-cpp fi -cd yaml-cpp-yaml-cpp-$YAML_CPP_VERSION +cd yaml-cpp mkdir -p build cd build echo "Building YAML-CPP..." -cmake .. +cmake -DYAML_CPP_BUILD_TESTS=OFF -DYAML_CPP_BUILD_TOOLS=OFF -DYAML_CPP_BUILD_CONTRIB=OFF .. make $PARALLEL cd ../.. @@ -67,10 +71,11 @@ git checkout $CSVPARSER_COMMIT cd .. echo "Getting PEGTL..." -if [ ! -d PEGTL-$PEGTL_VERSION ] ; then +if [ ! -d PEGTL ] ; then wget -O pegtl.tar.gz https://github.com/taocpp/PEGTL/archive/$PEGTL_VERSION.tar.gz tar -xf pegtl.tar.gz rm pegtl.tar.gz + mv PEGTL-$PEGTL_VERSION PEGTL fi if [ "$ENABLE_TESTS" = "1" ]; then diff --git a/snap/.gitignore b/snap/.gitignore deleted file mode 100644 index 48a6af0..0000000 --- a/snap/.gitignore +++ /dev/null @@ -1 +0,0 @@ -.snapcraft diff --git a/snap/snapcraft.yaml b/snap/snapcraft.yaml index e0d9945..145d697 100644 --- a/snap/snapcraft.yaml +++ b/snap/snapcraft.yaml @@ -1,25 +1,31 @@ name: timetabler -version: "0.3.0+git" +version: git +version-script: + ./gen_version.sh . 1 summary: Timetable scheduling software using MaxSAT solver. description: | A highly customizable timetabling software for educational institutions that encodes timetabling constraints as a SAT formula and solves them using a MaxSAT solver. type: app -# Set grade to devel in other commits and stable in release commits -grade: devel +grade: stable confinement: strict apps: timetabler: command: timetabler + plugs: [home] parts: timetabler: plugin: cmake - prepare: bash ../src/install_dependencies.sh + override-build: | + cd ../src/ + bash install_dependencies.sh --parallel + cd - + snapcraftctl build configflags: - - -DOPEN_WBO_PATH=dependencies/open-wbo - - -DYAML_CPP_PATH=dependencies/yaml-cpp-yaml-cpp-0.6.2 - - -DCSVPARSER_PATH=dependencies/CSVparser - - -DPEGTL_PATH=dependencies/PEGTL-2.7.0 + - -DOPEN_WBO_PATH=../src/dependencies/open-wbo + - -DYAML_CPP_PATH=../src/dependencies/yaml-cpp + - -DCSVPARSER_PATH=../src/dependencies/CSVparser + - -DPEGTL_PATH=../src/dependencies/PEGTL diff --git a/src/clauses.cpp b/src/clauses.cpp index 5ba02f7..e3637ee 100644 --- a/src/clauses.cpp +++ b/src/clauses.cpp @@ -28,6 +28,13 @@ Clauses::Clauses(const CClause &clause) { clauses.push_back(clause); } +Clauses::Clauses(const vec &lits) { + clauses.clear(); + for (int i = 0; i < lits.size(); i++) { + clauses.push_back(CClause(lits[i])); + } +} + /** * @brief Constructs the Clauses object. * diff --git a/src/constraint_adder.cpp b/src/constraint_adder.cpp index fd00434..f24438a 100644 --- a/src/constraint_adder.cpp +++ b/src/constraint_adder.cpp @@ -116,19 +116,19 @@ Clauses ConstraintAdder::programSingleCoreCourseAtATime() { * * @return A Clauses object describing the constraint */ -Clauses ConstraintAdder::minorInMinorTime() { - Clauses result; - result.clear(); +std::vector ConstraintAdder::minorInMinorTime() { std::vector courses = timetabler->data.courses; + std::vector 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.addClauses(antecedent >> consequent); - result.addClauses(consequent >> antecedent); + result[i].addClauses(antecedent >> consequent); + result[i].addClauses(consequent >> antecedent); } return result; } @@ -147,11 +147,12 @@ Clauses ConstraintAdder::minorInMinorTime() { * * @return A Clauses object describing the constraint */ -Clauses ConstraintAdder::exactlyOneFieldValuePerCourse(FieldType fieldType) { - Clauses result; - result.clear(); +std::vector ConstraintAdder::exactlyOneFieldValuePerCourse( + FieldType fieldType) { std::vector courses = timetabler->data.courses; + std::vector 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); @@ -159,7 +160,7 @@ Clauses ConstraintAdder::exactlyOneFieldValuePerCourse(FieldType 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.addClauses(cclause >> exactlyOneFieldValue); + result[i].addClauses(cclause >> exactlyOneFieldValue); } return result; } @@ -170,16 +171,30 @@ Clauses ConstraintAdder::exactlyOneFieldValuePerCourse(FieldType fieldType) { * @param[in] clauseType The PredefinedClauses member denoting the constraint * type * @param[in] clauses The clauses to be added + * @param[in] course The corresponding course index (-1 for if there is no + * corresponding course) */ void ConstraintAdder::addSingleConstraint(PredefinedClauses clauseType, - const Clauses &clauses) { - if (timetabler->data.predefinedClausesWeights[clauseType] != 0) { - Clauses hardConsequent = - CClause(timetabler->data.predefinedConstraintVars[clauseType]) >> - clauses; - timetabler->addClauses(hardConsequent, -1); + 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); } - timetabler->addHighLevelConstraintClauses(clauseType); } /** @@ -190,30 +205,63 @@ void ConstraintAdder::addConstraints() { std::vector weights = timetabler->data.predefinedClausesWeights; // add the constraints to the formula addSingleConstraint(PredefinedClauses::instructorSingleCourseAtATime, - instructorSingleCourseAtATime()); + instructorSingleCourseAtATime(), -1); addSingleConstraint(PredefinedClauses::classroomSingleCourseAtATime, - classroomSingleCourseAtATime()); + classroomSingleCourseAtATime(), -1); addSingleConstraint(PredefinedClauses::programSingleCoreCourseAtATime, - programSingleCoreCourseAtATime()); - addSingleConstraint(PredefinedClauses::minorInMinorTime, minorInMinorTime()); - addSingleConstraint(PredefinedClauses::programAtMostOneOfCoreOrElective, - programAtMostOneOfCoreOrElective()); + 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); + } - addSingleConstraint(PredefinedClauses::exactlyOneSlotPerCourse, - exactlyOneFieldValuePerCourse(FieldType::slot)); - addSingleConstraint(PredefinedClauses::exactlyOneClassroomPerCourse, - exactlyOneFieldValuePerCourse(FieldType::classroom)); - addSingleConstraint(PredefinedClauses::exactlyOneInstructorPerCourse, - exactlyOneFieldValuePerCourse(FieldType::instructor)); - addSingleConstraint(PredefinedClauses::exactlyOneIsMinorPerCourse, - exactlyOneFieldValuePerCourse(FieldType::isMinor)); - addSingleConstraint(PredefinedClauses::exactlyOneSegmentPerCourse, - exactlyOneFieldValuePerCourse(FieldType::segment)); + 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); + } - addSingleConstraint(PredefinedClauses::coreInMorningTime, - coreInMorningTime()); - addSingleConstraint(PredefinedClauses::electiveInNonMorningTime, - electiveInNonMorningTime()); + clauses = electiveInNonMorningTime(); + for (unsigned i = 0; i < clauses.size(); i++) { + addSingleConstraint(PredefinedClauses::electiveInNonMorningTime, clauses[i], + i); + } } /*Clauses ConstraintAdder::softConstraints() { @@ -227,14 +275,14 @@ void ConstraintAdder::addConstraints() { * * @return A Clauses object describing the constraint */ -Clauses ConstraintAdder::coreInMorningTime() { - Clauses result; - result.clear(); +std::vector ConstraintAdder::coreInMorningTime() { std::vector courses = timetabler->data.courses; + std::vector 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.addClauses(coreCourse >> morningTime); + result[i].addClauses(coreCourse >> morningTime); } return result; } @@ -246,14 +294,14 @@ Clauses ConstraintAdder::coreInMorningTime() { * * @return A Clauses object describing the constraint */ -Clauses ConstraintAdder::electiveInNonMorningTime() { - Clauses result; - result.clear(); +std::vector ConstraintAdder::electiveInNonMorningTime() { std::vector courses = timetabler->data.courses; + std::vector 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.addClauses(coreCourse >> (~morningTime)); + result[i].addClauses(coreCourse >> (~morningTime)); } return result; } @@ -267,12 +315,12 @@ Clauses ConstraintAdder::electiveInNonMorningTime() { * * @return A Clauses object describing the constraint */ -Clauses ConstraintAdder::programAtMostOneOfCoreOrElective() { - Clauses result; - result.clear(); +std::vector ConstraintAdder::programAtMostOneOfCoreOrElective() { std::vector courses = timetabler->data.courses; + std::vector result(courses.size()); for (unsigned i = 0; i < courses.size(); i++) { - result.addClauses(encoder->programAtMostOneOfCoreOrElective(i)); + result[i].clear(); + result[i].addClauses(encoder->programAtMostOneOfCoreOrElective(i)); } return result; } diff --git a/src/constraint_encoder.cpp b/src/constraint_encoder.cpp index 5d3bb63..3ead78e 100644 --- a/src/constraint_encoder.cpp +++ b/src/constraint_encoder.cpp @@ -242,15 +242,7 @@ Clauses ConstraintEncoder::hasAtLeastOneFieldValueTrue(int course, Clauses ConstraintEncoder::hasAtMostOneFieldValueTrue(int course, FieldType fieldType) { std::vector varsToUse = getAllowedVars(course, fieldType); - Clauses result; - for (unsigned i = 0; i < vars[course][fieldType].size(); i++) { - for (unsigned j = i + 1; j < vars[course][fieldType].size(); j++) { - Clauses first(vars[course][fieldType][i]); - Clauses second(vars[course][fieldType][j]); - Clauses negSecond = ~second; - result.addClauses(~first | negSecond); - } - } + Clauses result = timetabler->generateAtMostKTotalizerEncoding(varsToUse, 1); return result; } @@ -294,7 +286,8 @@ std::vector ConstraintEncoder::getAllowedVars(int course, * @return A Clauses object representing the condition */ Clauses ConstraintEncoder::isMinorCourse(int course) { - Clauses result(vars[course][FieldType::isMinor][MinorType::isMinorCourse]); + Clauses result(vars[course][FieldType::isMinor] + [static_cast(MinorType::isMinorCourse)]); return result; } diff --git a/src/custom_parser.cpp b/src/custom_parser.cpp index 5e2408a..41f403b 100644 --- a/src/custom_parser.cpp +++ b/src/custom_parser.cpp @@ -1,4 +1,5 @@ #include "custom_parser.h" + #include #include #include @@ -9,8 +10,103 @@ #include "global.h" #include "utils.h" +/** + * @brief Makes an antecedent. + * + * @param obj The object + * @param[in] course The course + * + * @return Clauses corresponding to the antecedent + */ +Clauses makeAntecedent(Object &obj, int course) { + Clauses ante, clause; + if (obj.instructorValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::instructor, obj.instructorValues); + ante = ante & clause; + } + if (obj.programValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::program, obj.programValues); + ante = ante & clause; + } + if (obj.segmentValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::segment, obj.segmentValues); + ante = ante & clause; + } + if (obj.isMinorValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::isMinor, obj.isMinorValues); + ante = ante & clause; + } + return ante; +} + +/** + * @brief Makes a consequent. + * + * @param obj The object + * @param[in] course The course + * @param[in] i Index of course in courseValues + * + * @return Clauses corresponding to the consequent + */ +Clauses makeConsequent(Object &obj, int course, int i) { + Clauses cons, clause; + if (obj.classSame) { + for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { + Clauses a = makeAntecedent(obj, obj.courseValues[j]); + Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( + course, obj.courseValues[j], FieldType::classroom); + a = a >> b; + cons = cons & a; + } + } + if (obj.classNotSame) { + for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { + Clauses a = makeAntecedent(obj, obj.courseValues[j]); + Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( + course, obj.courseValues[j], FieldType::classroom); + a = a >> (~b); + cons = cons & a; + } + } + if (obj.slotSame) { + for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { + Clauses a = makeAntecedent(obj, obj.courseValues[j]); + Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( + course, obj.courseValues[j], FieldType::slot); + a = a >> b; + cons = cons & a; + } + } + if (obj.slotNotSame) { + for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { + Clauses a = makeAntecedent(obj, obj.courseValues[j]); + Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( + course, obj.courseValues[j], FieldType::slot); + a = a >> (~b); + cons = cons & a; + } + } + if (obj.classValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::classroom, obj.classValues); + cons = cons & clause; + } + if (obj.slotValues.size() > 0) { + clause = obj.constraintEncoder->hasFieldTypeListedValues( + course, FieldType::slot, obj.slotValues); + cons = cons & clause; + } + return cons; +} + namespace pegtl = tao::TAO_PEGTL_NAMESPACE; +namespace custom_constraint_grammar { + template struct action : pegtl::nothing {}; @@ -179,7 +275,8 @@ struct action { struct value : pegtl::plus, pegtl::range<'A', 'Z'>, pegtl::digit, pegtl::one<'.'>, pegtl::one<'-'>, - pegtl::one<'@'>, pegtl::space>> {}; + pegtl::one<'@'>, pegtl::one<'<'>, pegtl::one<'>'>, + pegtl::space>> {}; template <> struct action { template @@ -432,99 +529,6 @@ struct fielddecl : pegtl::seq, values> {}; */ struct fielddecls : pegtl::opt> {}; -/** - * @brief Makes an antecedent. - * - * @param obj The object - * @param[in] course The course - * - * @return Clauses corresponding to the antecedent - */ -Clauses makeAntecedent(Object &obj, int course) { - Clauses ante, clause; - if (obj.instructorValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::instructor, obj.instructorValues); - ante = ante & clause; - } - if (obj.programValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::program, obj.programValues); - ante = ante & clause; - } - if (obj.segmentValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::segment, obj.segmentValues); - ante = ante & clause; - } - if (obj.isMinorValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::isMinor, obj.isMinorValues); - ante = ante & clause; - } - return ante; -} - -/** - * @brief Makes a consequent. - * - * @param obj The object - * @param[in] course The course - * @param[in] i Index of course in courseValues - * - * @return Clauses corresponding to the consequent - */ -Clauses makeConsequent(Object &obj, int course, int i) { - Clauses cons, clause; - if (obj.classSame) { - for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { - Clauses a = makeAntecedent(obj, obj.courseValues[j]); - Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( - course, obj.courseValues[j], FieldType::classroom); - a = a >> b; - cons = cons & a; - } - } - if (obj.classNotSame) { - for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { - Clauses a = makeAntecedent(obj, obj.courseValues[j]); - Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( - course, obj.courseValues[j], FieldType::classroom); - a = a >> (~b); - cons = cons & a; - } - } - if (obj.slotSame) { - for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { - Clauses a = makeAntecedent(obj, obj.courseValues[j]); - Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( - course, obj.courseValues[j], FieldType::slot); - a = a >> b; - cons = cons & a; - } - } - if (obj.slotNotSame) { - for (unsigned j = i + 1; j < obj.courseValues.size(); j++) { - Clauses a = makeAntecedent(obj, obj.courseValues[j]); - Clauses b = obj.constraintEncoder->hasSameFieldTypeAndValue( - course, obj.courseValues[j], FieldType::slot); - a = a >> (~b); - cons = cons & a; - } - } - if (obj.classValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::classroom, obj.classValues); - cons = cons & clause; - } - if (obj.slotValues.size() > 0) { - clause = obj.constraintEncoder->hasFieldTypeListedValues( - course, FieldType::slot, obj.slotValues); - cons = cons & clause; - } - return cons; -} - /** * @brief Parse a constraint */ @@ -564,6 +568,11 @@ struct action { obj.segmentValues.clear(); obj.classValues.clear(); obj.slotValues.clear(); + obj.isNot = false; + obj.classSame = false; + obj.slotSame = false; + obj.classNotSame = false; + obj.slotNotSame = false; } }; @@ -682,6 +691,7 @@ struct action { obj.constraint; obj.timetabler->addClauses(hardConsequent, -1); } + obj.timetabler->data.customMap[index] = course; obj.timetabler->addHighLevelCustomConstraintClauses(index, obj.integer); } obj.courseValues.clear(); @@ -691,6 +701,11 @@ struct action { obj.segmentValues.clear(); obj.classValues.clear(); obj.slotValues.clear(); + obj.isNot = false; + obj.classSame = false; + obj.slotSame = false; + obj.classNotSame = false; + obj.slotNotSame = false; } }; @@ -734,6 +749,16 @@ struct control : pegtl::normal { } }; +} // namespace custom_constraint_grammar + +/** + * @brief Parses custom constraints given in a file and adds them to the + * solver. + * + * @param[in] file The file containing the constraints + * @param constraintEncoder The ConstraintEncoder object + * @param timetabler The Timetabler object + */ void parseCustomConstraints(std::string file, ConstraintEncoder *constraintEncoder, Timetabler *timetabler) { @@ -741,7 +766,9 @@ void parseCustomConstraints(std::string file, obj.constraintEncoder = constraintEncoder; obj.timetabler = timetabler; pegtl::file_input<> in(file); - pegtl::parse(in, obj); + pegtl::parse(in, obj); } /** @@ -753,4 +780,4 @@ Object::Object() { slotSame = false; classNotSame = false; slotNotSame = false; -} \ No newline at end of file +} diff --git a/src/fields/course.cpp b/src/fields/course.cpp index d03123f..a33b893 100644 --- a/src/fields/course.cpp +++ b/src/fields/course.cpp @@ -17,7 +17,7 @@ * @param[in] isMinor Indicates if the course is a minor course */ Course::Course(std::string name, unsigned classSize, int instructor, - int segment, int isMinor) { + int segment, MinorType isMinor) { this->name = name; this->classSize = classSize; this->instructor = instructor; @@ -37,7 +37,7 @@ Course::Course(std::string name, unsigned classSize, int instructor, * applicable */ Course::Course(std::string name, unsigned classSize, int instructor, - int segment, int isMinor, std::vector programs) { + int segment, MinorType isMinor, std::vector programs) { this->name = name; this->classSize = classSize; this->instructor = instructor; @@ -63,8 +63,18 @@ void Course::setPrograms(std::vector programs) { */ void Course::addProgram(int programs) { this->programs.push_back(programs); } +/** + * @brief Adds a classroom that is applicable to the Course. + * + * @param[in] cr The index of the classroom to be added + */ void Course::addClassroom(int cr) { this->classroom = cr; } +/** + * @brief Adds a slot that is applicable to the Course. + * + * @param[in] s The index of the slot to be added + */ void Course::addSlot(int s) { this->slot = s; } /** @@ -112,10 +122,20 @@ int Course::getSegment() { return segment; } * * @return The isMinor index in the list of isMinors */ -int Course::getIsMinor() { return isMinor; } +MinorType Course::getIsMinor() { return isMinor; } +/** + * @brief Gets the 'classroom' index of the Course. + * + * @return The classroom index in the list of Classrooms + */ int Course::getClassroom() { return classroom; } +/** + * @brief Gets the 'slot' index of the Course. + * + * @return The slot index in the list of slots + */ int Course::getSlot() { return slot; } /** @@ -123,4 +143,4 @@ int Course::getSlot() { return slot; } * * @return The class size. */ -unsigned Course::getClassSize() { return classSize; } \ No newline at end of file +unsigned Course::getClassSize() { return classSize; } diff --git a/src/main.cpp b/src/main.cpp index d229ee0..7464372 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -13,6 +13,11 @@ #include "utils.h" #include "version.h" +/** + * @brief Display information about timetabler + * + * @param[in] display_desc If true, also prints the description + */ void display_meta(bool display_desc = false) { std::cout << "Timetabler version " __TIMETABLER_VERSION__ << std::endl; if (display_desc) @@ -23,6 +28,9 @@ void display_meta(bool display_desc = false) { << std::endl; } +/** + * Options supported in command line interface + */ const struct option long_options[] = {{"help", no_argument, 0, 'h'}, {"fields", required_argument, 0, 'f'}, {"input", required_argument, 0, 'i'}, @@ -32,6 +40,9 @@ const struct option long_options[] = {{"help", no_argument, 0, 'h'}, {"version", no_argument, 0, 'v'}, {0, 0, 0, 0}}; +/** + * Descriptions of the options supported in CLI + */ const std::string option_desc[] = {"display this help", "fields yaml file", "input csv file", @@ -41,6 +52,11 @@ const std::string option_desc[] = {"display this help", "display version", ""}; +/** + * @brief Display help for CLI options. + * + * @param[in] exec Name of the executable + */ void display_help(std::string exec = "timetabler") { display_meta(true); std::cout << "\nUsage:\n"; @@ -59,6 +75,11 @@ void display_help(std::string exec = "timetabler") { } } +/** + * @brief Display error message when unrecognised option is given in CLI + * + * @param[in] err The error message + */ void display_error(std::string err) { std::cout << err << std::endl; std::cout << "Use --help option to know about supported options." @@ -68,6 +89,14 @@ void display_error(std::string err) { Timetabler *timetabler; +/** + * @brief The main function + * + * @param[in] argc Count of the cli arguments + * @param argv Arguments passed through cli + * + * @return Exit code when program ends + */ int main(int argc, char *const *argv) { std::string input_file, fields_file, custom_file, output_file; unsigned verbosity = 3; @@ -136,6 +165,7 @@ int main(int argc, char *const *argv) { constraintAdder.addConstraints(); if (custom_file != "") { parseCustomConstraints(custom_file, &encoder, timetabler); + LOG(INFO) << "Custom constraints parsed."; } timetabler->addHighLevelClauses(); timetabler->addExistingAssignments(); diff --git a/src/parser.cpp b/src/parser.cpp index fb146f2..793f561 100644 --- a/src/parser.cpp +++ b/src/parser.cpp @@ -163,12 +163,12 @@ void Parser::parseInput(std::string file) { LOG(ERROR) << "Input contains invalid Segment name"; } std::string isMinorStr = parser[i]["is_minor"]; - int isMinor; - if (isMinorStr == "Yes") { - isMinor = 0; + MinorType isMinor = MinorType::isMinorCourse; + if (isMinorStr == "Yes" || isMinorStr == "Y") { + isMinor = MinorType::isMinorCourse; assignmentsThisCourse[FieldType::isMinor].push_back(l_True); - } else if (isMinorStr == "No") { - isMinor = 1; + } else if (isMinorStr == "No" || isMinorStr == "N" || isMinorStr == "") { + isMinor = MinorType::isNotMinorCourse; assignmentsThisCourse[FieldType::isMinor].push_back(l_False); } else { LOG(ERROR) << "Input contains invalid IsMinor value (should be " @@ -178,15 +178,17 @@ void Parser::parseInput(std::string file) { for (unsigned j = 0; j < timetabler->data.programs.size(); j += 2) { std::string s = timetabler->data.programs[j].getName(); - if (parser[i][s] == "Core") { + if (parser[i][s] == "Core" || parser[i][s] == "C" || + parser[i][s] == "Y") { course.addProgram(j); assignmentsThisCourse[FieldType::program].push_back(l_True); assignmentsThisCourse[FieldType::program].push_back(l_False); - } else if (parser[i][s] == "Elective") { + } else if (parser[i][s] == "Elective" || parser[i][s] == "E") { course.addProgram(j + 1); assignmentsThisCourse[FieldType::program].push_back(l_False); assignmentsThisCourse[FieldType::program].push_back(l_True); - } else if (parser[i][s] == "No") { + } else if (parser[i][s] == "No" || parser[i][s] == "N" || + parser[i][s] == "") { assignmentsThisCourse[FieldType::program].push_back(l_False); assignmentsThisCourse[FieldType::program].push_back(l_False); } else { @@ -236,10 +238,16 @@ void Parser::parseInput(std::string file) { } } +/** + * @brief Verifies if the input is valid. + * + * @return True, if the input is valid. + */ bool Parser::verify() { bool result = true; for (auto course1 : timetabler->data.courses) { - if (course1.getIsMinor() && course1.getSlot() != -1) { + if (course1.getIsMinor() == MinorType::isMinorCourse && + course1.getSlot() != -1) { if (timetabler->data.slots[course1.getSlot()].isMinorSlot()) { if (timetabler->data.predefinedClausesWeights [PredefinedClauses::minorInMinorTime] != 0) { @@ -368,8 +376,20 @@ void Parser::addVars() { } timetabler->data.highLevelVars.push_back(highLevelCourseVars); } + + timetabler->data.predefinedConstraintVars.resize( + Global::PREDEFINED_CLAUSES_COUNT); for (unsigned i = 0; i < Global::PREDEFINED_CLAUSES_COUNT; i++) { - Var v = timetabler->newVar(); - timetabler->data.predefinedConstraintVars.push_back(v); + if (i == PredefinedClauses::instructorSingleCourseAtATime || + i == PredefinedClauses::classroomSingleCourseAtATime || + i == PredefinedClauses::programSingleCoreCourseAtATime) { + Var v = timetabler->newVar(); + timetabler->data.predefinedConstraintVars[i].push_back(v); + } else { + for (unsigned j = 0; j < timetabler->data.courses.size(); j++) { + Var v = timetabler->newVar(); + timetabler->data.predefinedConstraintVars[i].push_back(v); + } + } } -} \ No newline at end of file +} diff --git a/src/timetabler.cpp b/src/timetabler.cpp index fad4545..c7afab5 100644 --- a/src/timetabler.cpp +++ b/src/timetabler.cpp @@ -1,5 +1,6 @@ #include "timetabler.h" +#include "Encoder.h" #include #include #include @@ -66,13 +67,28 @@ void Timetabler::addHighLevelClauses() { * with weight as specified for the constraint. * * @param[in] clauseType The clause type + * @param[in] course The corresponding course index (-1 for if there is no + * corresponding course) */ -void Timetabler::addHighLevelConstraintClauses(PredefinedClauses clauseType) { - Lit l = mkLit(data.predefinedConstraintVars[clauseType], false); - if (data.predefinedClausesWeights[clauseType] != 0) { - addToFormula(l, data.predefinedClausesWeights[clauseType]); +void Timetabler::addHighLevelConstraintClauses(PredefinedClauses clauseType, + const int course) { + if (course == -1) { + assert(data.predefinedConstraintVars[clauseType].size() == 1); + Lit l = mkLit(data.predefinedConstraintVars[clauseType][0], false); + if (data.predefinedClausesWeights[clauseType] != 0) { + addToFormula(l, data.predefinedClausesWeights[clauseType]); + } else { + addToFormula(l, -1); + } } else { - addToFormula(l, -1); + assert(data.predefinedConstraintVars[clauseType].size() == + data.courses.size()); + Lit l = mkLit(data.predefinedConstraintVars[clauseType][course], false); + if (data.predefinedClausesWeights[clauseType] != 0) { + addToFormula(l, data.predefinedClausesWeights[clauseType]); + } else { + addToFormula(l, -1); + } } } @@ -201,6 +217,26 @@ bool Timetabler::checkAllTrue(const std::vector &inputs) { return true; } +/** + * @brief Checks if a given set of variables (in 2D vector) are true in the + * model returned by the solver. + * + * @param[in] inputs The input variables + * + * @return True, if all variables are True, False otherwise + */ +bool Timetabler::checkAllTrue(const std::vector> &inputs) { + if (model.size() == 0) { + return false; + } + for (auto &i : inputs) { + for (auto &j : i) { + if (model[j] == l_False) return false; + } + } + return true; +} + /** * @brief Determines if a given variable is true in the model returned by * the solver. @@ -416,7 +452,7 @@ void Timetabler::displayUnsatisfiedOutputReasons() { } } for (unsigned i = 0; i < data.predefinedConstraintVars.size(); i++) { - if (!isVarTrue(data.predefinedConstraintVars[i]) && + if (!checkAllTrue(data.predefinedConstraintVars[i]) && data.predefinedClausesWeights[i] != 0) { LOG(WARNING) << "Predefined Constraint : " << Utils::getPredefinedConstraintName(PredefinedClauses(i)) @@ -425,12 +461,26 @@ void Timetabler::displayUnsatisfiedOutputReasons() { } for (unsigned i = 0; i < data.customConstraintVars.size(); i++) { if (!isVarTrue(data.customConstraintVars[i])) { - LOG(WARNING) << "Custom Constraint : " << i + 1 + LOG(WARNING) << "Custom Constraint : " << i + 1 << " for course " + << data.courses[data.customMap[i + 1]].getName() << " could not be satisfied"; } } } +Clauses Timetabler::generateAtMostKTotalizerEncoding( + const std::vector &relaxationVars, int64_t rhs) { + vec encodingLits; + vec encodingAssumptions; + for (auto &v : relaxationVars) { + encodingLits.push(mkLit(v, false)); + } + TTotalizer totalizerEncoder; + totalizerEncoder.build(formula, encodingLits, rhs); + totalizerEncoder.update(formula, rhs, encodingLits, encodingAssumptions); + return Clauses(encodingAssumptions); +} + /** * @brief Destroys the object, and deletes the solver. */ diff --git a/src/totalizer.cpp b/src/totalizer.cpp new file mode 100644 index 0000000..6948cde --- /dev/null +++ b/src/totalizer.cpp @@ -0,0 +1,256 @@ +/*! + * \author Ruben Martins - ruben@sat.inesc-id.pt + * + * @section LICENSE + * + * Open-WBO, Copyright (c) 2013-2017, Ruben Martins, Vasco Manquinho, Ines Lynce + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + */ + +#include "totalizer.h" +#include "utils.h" + +using namespace NSPACE; +using namespace openwbo; + +void TTotalizer::addUnitClause(MaxSATFormula *formula, Lit a) { + assert(a != lit_Undef); + assert(var(a) < formula->nVars()); + vec clause; + clause.push(a); + formula->addHardClause(clause); +} + +void TTotalizer::addBinaryClause(MaxSATFormula *formula, Lit a, Lit b) { + assert(a != lit_Undef && b != lit_Undef); + assert(var(a) < formula->nVars() && var(b) < formula->nVars()); + vec clause; + clause.push(a); + clause.push(b); + formula->addHardClause(clause); +} + +void TTotalizer::addTernaryClause(MaxSATFormula *formula, Lit a, Lit b, Lit c) { + assert(a != lit_Undef && b != lit_Undef && c != lit_Undef); + assert(var(a) < formula->nVars() && var(b) < formula->nVars() && + var(c) < formula->nVars()); + vec clause; + assert(clause.size() == 0); + clause.push(a); + clause.push(b); + clause.push(c); + formula->addHardClause(clause); +} + +void TTotalizer::newSATVariable(MaxSATFormula *formula) { formula->newVar(); } + +void TTotalizer::incremental(MaxSATFormula *formula, int64_t rhs) { + for (int z = 0; z < totalizerIterative_rhs.size(); z++) { + // We only need to count the sums up to k. + for (int i = 0; i <= totalizerIterative_left[z].size(); i++) { + for (int j = 0; j <= totalizerIterative_right[z].size(); j++) { + if (i == 0 && j == 0) { + continue; + } + + if (i + j > rhs + 1 || i + j <= totalizerIterative_rhs[z] + 1) { + continue; + } + + if (i == 0) { + addBinaryClause(formula, ~(totalizerIterative_right[z])[j - 1], + (totalizerIterative_output[z])[j - 1]); + n_clauses++; + } else if (j == 0) { + addBinaryClause(formula, ~(totalizerIterative_left[z])[i - 1], + (totalizerIterative_output[z])[i - 1]); + n_clauses++; + } else { + addTernaryClause(formula, ~(totalizerIterative_left[z])[i - 1], + ~(totalizerIterative_right[z])[j - 1], + (totalizerIterative_output[z])[i + j - 1]); + n_clauses++; + } + } + } + totalizerIterative_rhs[z] = rhs; + } +} + +void TTotalizer::adder(MaxSATFormula *formula, vec &left, vec &right, + vec &output) { + assert(output.size() == left.size() + right.size()); + if (incremental_strategy == _INCREMENTAL_ITERATIVE_) { + totalizerIterative_left.push(); + new (&totalizerIterative_left[totalizerIterative_left.size() - 1]) + vec(); + left.copyTo(totalizerIterative_left.last()); + totalizerIterative_right.push(); + new (&totalizerIterative_right[totalizerIterative_right.size() - 1]) + vec(); + right.copyTo(totalizerIterative_right.last()); + totalizerIterative_output.push(); + new (&totalizerIterative_output[totalizerIterative_output.size() - 1]) + vec(); + output.copyTo(totalizerIterative_output.last()); + totalizerIterative_rhs.push(current_cardinality_rhs); + } + + // We only need to count the sums up to k. + for (int i = 0; i <= left.size(); i++) { + for (int j = 0; j <= right.size(); j++) { + if (i == 0 && j == 0) continue; + + if (i + j > current_cardinality_rhs + 1) continue; + + if (i == 0) { + addBinaryClause(formula, ~right[j - 1], output[j - 1]); + n_clauses++; + } else if (j == 0) { + addBinaryClause(formula, ~left[i - 1], output[i - 1]); + n_clauses++; + } else { + addTernaryClause(formula, ~left[i - 1], ~right[j - 1], + output[i + j - 1]); + n_clauses++; + } + } + } +} + +void TTotalizer::toCNF(MaxSATFormula *formula, vec &lits) { + vec left; + vec right; + + assert(lits.size() > 1); + int split = floor(lits.size() / 2); + + for (int i = 0; i < lits.size(); i++) { + if (i < split) { + // left branch + if (split == 1) { + assert(cardinality_inlits.size() > 0); + left.push(cardinality_inlits.last()); + cardinality_inlits.pop(); + } else { + Lit p = mkLit(formula->nVars(), false); + newSATVariable(formula); + left.push(p); + } + } else { + // right branch + if (lits.size() - split == 1) { + assert(cardinality_inlits.size() > 0); + right.push(cardinality_inlits.last()); + cardinality_inlits.pop(); + } else { + Lit p = mkLit(formula->nVars(), false); + newSATVariable(formula); + right.push(p); + } + } + } + + if (left.size() > 1) toCNF(formula, left); + if (right.size() > 1) toCNF(formula, right); + adder(formula, left, right, lits); +} + +void TTotalizer::update(MaxSATFormula *formula, int64_t rhs, vec &lits, + vec &assumptions) { + assert(hasEncoding); + + // incremental(formula, rhs); + assumptions.clear(); + for (int i = rhs; i < cardinality_outlits.size(); i++) + assumptions.push(~cardinality_outlits[i]); +} + +/*_________________________________________________________________________________________________ + | + | build : (S : MaxSATFormula *) (lits : vec&) (int64_t : rhs) -> [void] + | + | Description: + | + | Builds a cardinality constraint of the kind x_1 + ... x_n <= k. + | Uses the totalizer encoding for translation the cardinality constraint + into CNF. + | Does not impose any constraints on the value of 'k'. + | NOTE: Use method 'update' to impose a restriction on the value of 'k'. + | + | For further details see: + | * Olivier Bailleux, Yacine Boufkhad: Efficient CNF Encoding of Boolean + Cardinality Constraints. CP 2003: 108-122 + | + | Pre-conditions: + | * Assumes that 'lits' is not empty and 'rhs' is larger or equal to 0. + | + | Post-conditions: + | * 'S' is updated with the clauses that encode the cardinality constraint. + | * hasEncoding is set to 'true'. + | + |________________________________________________________________________________________________@*/ +void TTotalizer::build(MaxSATFormula *formula, vec &lits, int64_t rhs) { + cardinality_outlits.clear(); + hasEncoding = false; + + if (rhs == 0) { + for (int i = 0; i < lits.size(); i++) addUnitClause(formula, ~lits[i]); + return; + } + + assert(rhs >= 1 && rhs <= lits.size()); + + if (incremental_strategy == _INCREMENTAL_NONE_ && rhs == lits.size()) { + DEBUG() << "Totalizer (Not incremental): Rhs is equal to lits.size()"; + hasEncoding = true; + return; + } + + if (rhs == lits.size() && !joinMode) return; + + for (int i = 0; i < lits.size(); i++) { + Lit p = mkLit(formula->nVars(), false); + newSATVariable(formula); + cardinality_outlits.push(p); + } + + lits.copyTo(cardinality_inlits); + current_cardinality_rhs = rhs; + + // If incremental blocking is enable then all clauses will contain a + // blocking literal 'b'. Setting this literal to 'true' is the same as + // deletting these clauses. + if (incremental_strategy == _INCREMENTAL_BLOCKING_) { + Lit p = mkLit(formula->nVars(), false); + newSATVariable(formula); + if (blocking != lit_Undef) disable_lits.push(blocking); + blocking = p; + } + + toCNF(formula, cardinality_outlits); + assert(cardinality_inlits.size() == 0); + + if (!joinMode) joinMode = true; + hasEncoding = true; + + lits.copyTo(ilits); +} diff --git a/src/tsolver.cpp b/src/tsolver.cpp index 320b373..768df00 100644 --- a/src/tsolver.cpp +++ b/src/tsolver.cpp @@ -76,6 +76,18 @@ std::vector TSolver::tSearch() { } } +// void TSolver::encodeAtMostK(vec &lits, vec &assumptions, +// int64_t rhs) { + +// } + +Var TSolver::newVar() { return solver->newVar(); } + +Lit TSolver::newLiteral(bool sign) { + Var v = solver->newVar(); + return mkLit(v, sign); +} + /** * @brief Solves a weighted MaxSAT problem *