Use Open WBO totalizer encoding for At Most One constraints

.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

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")
 

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
 

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

include/clauses.h

@@ -29,6 +29,7 @@ class Clauses {
 
  public:
   Clauses(const std::vector<CClause> &);
+  Clauses(const vec<Lit> &);
   Clauses(const CClause &);
   Clauses(const Lit &);
   Clauses(const Var &);

include/constraint_adder.h

@@ -36,20 +36,21 @@ class ConstraintAdder {
    */
   Timetabler *timetabler;
   Clauses fieldSingleValueAtATime(FieldType);
-  Clauses exactlyOneFieldValuePerCourse(FieldType);
+  std::vector<Clauses> exactlyOneFieldValuePerCourse(FieldType);
   Clauses instructorSingleCourseAtATime();
   Clauses classroomSingleCourseAtATime();
   Clauses programSingleCoreCourseAtATime();
-  Clauses minorInMinorTime();
-  Clauses coreInMorningTime();
-  Clauses electiveInNonMorningTime();
-  Clauses existingAssignmentClauses();
-  Clauses programAtMostOneOfCoreOrElective();
+  std::vector<Clauses> minorInMinorTime();
+  std::vector<Clauses> coreInMorningTime();
+  std::vector<Clauses> electiveInNonMorningTime();
+  // Clauses existingAssignmentClauses();
+  std::vector<Clauses> programAtMostOneOfCoreOrElective();
 
  public:
   ConstraintAdder(ConstraintEncoder *, Timetabler *);
   void addConstraints();
-  void addSingleConstraint(PredefinedClauses, const Clauses &);
+  void addSingleConstraint(PredefinedClauses, const Clauses &,
+                           const int course);
 };
 
 #endif

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);

include/data.h

@@ -3,6 +3,7 @@
 #ifndef DATA_H
 #define DATA_H
 
+#include <map>
 #include <string>
 #include <vector>
 #include "core/Solver.h"
@@ -78,7 +79,13 @@ class Data {
    * can make the necessary changes.
    */
   std::vector<std::vector<Var>> highLevelVars;
-  std::vector<Var> predefinedConstraintVars;
+  /**
+   * Stores the high level variables associated with the predefined constraints.
+   */
+  std::vector<std::vector<Var>> predefinedConstraintVars;
+  /**
+   * Stores the high level variables associated with the custom constraints.
+   */
   std::vector<Var> customConstraintVars;
   /**
    * Stores the existing assignments for every Course and
@@ -115,6 +122,10 @@ class Data {
    * or to disable certain constraints.
    */
   std::vector<int> predefinedClausesWeights;
+  /**
+   * Stores the course with the associated custom constraint.
+   */
+  std::map<int, unsigned> customMap;
   Data();
 };
 

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<int>);
+  Course(std::string, unsigned, int, int, MinorType);
+  Course(std::string, unsigned, int, int, MinorType, std::vector<int>);
   void setPrograms(std::vector<int>);
   void addProgram(int);
   void addClassroom(int);
@@ -64,7 +64,7 @@ class Course {
   int getInstructor();
   std::vector<int> getPrograms();
   int getSegment();
-  int getIsMinor();
+  MinorType getIsMinor();
   int getClassroom();
   int getSlot();
   unsigned getClassSize();

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
    */

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,

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

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<CClause> &, int);
   void addClauses(const Clauses &, int);
   bool checkAllTrue(const std::vector<Var> &);
+  bool checkAllTrue(const std::vector<std::vector<Var>> &);
   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<Lit> &, int);
   void addToFormula(Lit, int);
   void displayChangesInGivenAssignment();
+  Clauses generateAtMostKTotalizerEncoding(const std::vector<Var> &,
+                                             int64_t rhs = 1);
 };
 
 #endif

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<Lit> &lits, int64_t rhs);
+    void join(MaxSATFormula *formula, vec<Lit> &lits, int64_t rhs);
+    void update(MaxSATFormula *formula, int64_t rhs, vec<Lit> &lits,
+                vec<Lit> &assumptions);
+    void update(MaxSATFormula *formula, int64_t rhs) {
+        vec<Lit> lits;
+        vec<Lit> 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<Lit> &lits() { return ilits; }
+    vec<Lit> &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<Lit> &lits);
+    void adder(MaxSATFormula *formula, vec<Lit> &left, vec<Lit> &right,
+               vec<Lit> &output);
+    void incremental(MaxSATFormula *formula, int64_t rhs);
+    void toCNF(MaxSATFormula *formula, vec<Lit> &lits);
+
+    vec<vec<Lit>> totalizerIterative_left;
+    vec<vec<Lit>> totalizerIterative_right;
+    vec<vec<Lit>> totalizerIterative_output;
+    vec<int64_t> totalizerIterative_rhs;
+
+    Lit blocking; // Controls the blocking literal for the incremental blocking.
+    bool hasEncoding;
+
+    // TEMP
+    vec<Lit> ilits;
+    vec<Lit> olits;
+
+    vec<Lit>
+        cardinality_inlits; // Stores the inputs of the cardinality
+                            // constraint encoding for the totalizer encoding
+    vec<Lit> cardinality_outlits; // Stores the outputs of the cardinality
+                                  // constraint encoding for incremental solving
+
+    int incremental_strategy;
+    int64_t current_cardinality_rhs;
+
+    vec<Lit>
+        disable_lits; // Contains a vector with a list of blocking literals.
+    bool joinMode;
+
+    int n_clauses;
+    int n_variables;
+};
+
+#endif

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<lbool> tSearch();
-  void tWeighted();
+  public:
+    TSolver(int, int);
+    std::vector<lbool> tSearch();
+    void tWeighted();
+    // void encodeAtMostK(vec<Lit> &lits, vec<Lit> &assumptions, int64_t rhs =
+    // 1);
+    Var newVar();
+    Lit newLiteral(bool sign = false);
 };
 
 #endif