always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add overload checker to scheduling sat; more cleanup on the internals of sat

Browse Source
This commit is contained in:
Laurent Perron
2016-11-04 09:52:55 +01:00
parent 219a1353cf
commit 1ca88068e6
8 changed files with 534 additions and 129 deletions
Download Patch File Download Diff File Expand all files Collapse all files

202
makefiles/Makefile.gen.mk
View File

@@ -6,8 +6,8 @@ BASE_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -32,17 +32,17 @@ BASE_LIB_OBJS = \
$(OBJ_DIR)/base/stringprintf.$O \
$(OBJ_DIR)/base/sysinfo.$O \
$(OBJ_DIR)/base/threadpool.$O \
$(OBJ_DIR)/base/time_support.$O \
$(OBJ_DIR)/base/timer.$O
$(SRC_DIR)/base/adjustable_priority_queue-inl.h: \
$(SRC_DIR)/base/adjustable_priority_queue.h
$(OBJ_DIR)/base/timer.$O \
$(OBJ_DIR)/base/time_support.$O
$(SRC_DIR)/base/adjustable_priority_queue.h: \
$(SRC_DIR)/base/basictypes.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h
$(SRC_DIR)/base/adjustable_priority_queue-inl.h: \
$(SRC_DIR)/base/adjustable_priority_queue.h
$(SRC_DIR)/base/basictypes.h: \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h
@@ -153,15 +153,15 @@ $(SRC_DIR)/base/sysinfo.h: \
$(SRC_DIR)/base/thorough_hash.h: \
$(SRC_DIR)/base/integral_types.h
$(SRC_DIR)/base/time_support.h: \
$(SRC_DIR)/base/integral_types.h
$(SRC_DIR)/base/timer.h: \
$(SRC_DIR)/base/basictypes.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/base/time_support.h
$(SRC_DIR)/base/time_support.h: \
$(SRC_DIR)/base/integral_types.h
$(OBJ_DIR)/base/bitmap.$O: \
$(SRC_DIR)/base/bitmap.cc \
$(SRC_DIR)/base/basictypes.h \
@@ -249,16 +249,16 @@ $(OBJ_DIR)/base/threadpool.$O: \
$(SRC_DIR)/base/threadpool.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/base/threadpool.cc $(OBJ_OUT)$(OBJ_DIR)$Sbase$Sthreadpool.$O
$(OBJ_DIR)/base/time_support.$O: \
$(SRC_DIR)/base/time_support.cc \
$(SRC_DIR)/base/time_support.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/base/time_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sbase$Stime_support.$O
$(OBJ_DIR)/base/timer.$O: \
$(SRC_DIR)/base/timer.cc \
$(SRC_DIR)/base/timer.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/base/timer.cc $(OBJ_OUT)$(OBJ_DIR)$Sbase$Stimer.$O
$(OBJ_DIR)/base/time_support.$O: \
$(SRC_DIR)/base/time_support.cc \
$(SRC_DIR)/base/time_support.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/base/time_support.cc $(OBJ_OUT)$(OBJ_DIR)$Sbase$Stime_support.$O
UTIL_DEPS = \
$(SRC_DIR)/util/bitset.h \
$(SRC_DIR)/util/running_stat.h \
@@ -270,8 +270,8 @@ UTIL_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -375,8 +375,8 @@ $(SRC_DIR)/util/time_limit.h: \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/base/port.h \
$(SRC_DIR)/base/time_support.h \
$(SRC_DIR)/base/timer.h
$(SRC_DIR)/base/timer.h \
$(SRC_DIR)/base/time_support.h
$(SRC_DIR)/util/tuple_set.h: \
$(SRC_DIR)/base/hash.h \
@@ -495,8 +495,8 @@ LP_DATA_DEPS = \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/matrix_scaler.h \
$(SRC_DIR)/lp_data/permutation.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_column.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_vector.h \
$(SRC_DIR)/util/bitset.h \
$(SRC_DIR)/util/running_stat.h \
@@ -508,8 +508,8 @@ LP_DATA_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -569,8 +569,8 @@ $(SRC_DIR)/lp_data/lp_utils.h: \
$(SRC_DIR)/lp_data/matrix_scaler.h: \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/macros.h
$(SRC_DIR)/lp_data/matrix_utils.h: \
@@ -595,6 +595,9 @@ $(SRC_DIR)/lp_data/proto_utils.h: \
$(SRC_DIR)/lp_data/lp_data.h \
$(GEN_DIR)/linear_solver/linear_solver.pb.h
$(SRC_DIR)/lp_data/sparse_column.h: \
$(SRC_DIR)/lp_data/sparse_vector.h
$(SRC_DIR)/lp_data/sparse.h: \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/permutation.h \
@@ -602,9 +605,6 @@ $(SRC_DIR)/lp_data/sparse.h: \
$(SRC_DIR)/util/return_macros.h \
$(SRC_DIR)/base/integral_types.h
$(SRC_DIR)/lp_data/sparse_column.h: \
$(SRC_DIR)/lp_data/sparse_vector.h
$(SRC_DIR)/lp_data/sparse_vector.h: \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/permutation.h \
@@ -721,8 +721,8 @@ GLOP_DEPS = \
$(SRC_DIR)/glop/revised_simplex.h \
$(SRC_DIR)/glop/status.h \
$(SRC_DIR)/glop/update_row.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/util/bitset.h \
$(SRC_DIR)/util/running_stat.h \
$(SRC_DIR)/util/saturated_arithmetic.h \
@@ -733,8 +733,8 @@ GLOP_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -746,8 +746,8 @@ GLOP_DEPS = \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/matrix_scaler.h \
$(SRC_DIR)/lp_data/permutation.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_column.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_vector.h \
$(SRC_DIR)/linear_solver/linear_solver.h \
$(GEN_DIR)/linear_solver/linear_solver.pb.h
@@ -766,8 +766,8 @@ GLOP_LIB_OBJS = \
$(OBJ_DIR)/glop/revised_simplex.$O \
$(OBJ_DIR)/glop/status.$O \
$(OBJ_DIR)/glop/update_row.$O \
$(OBJ_DIR)/glop/variable_values.$O \
$(OBJ_DIR)/glop/variables_info.$O \
$(OBJ_DIR)/glop/variable_values.$O \
$(OBJ_DIR)/glop/parameters.pb.$O
$(SRC_DIR)/glop/basis_representation.h: \
@@ -872,8 +872,8 @@ $(SRC_DIR)/glop/revised_simplex.h: \
$(SRC_DIR)/glop/reduced_costs.h \
$(SRC_DIR)/glop/status.h \
$(SRC_DIR)/glop/update_row.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/util/time_limit.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/macros.h \
@@ -893,16 +893,16 @@ $(SRC_DIR)/glop/update_row.h: \
$(SRC_DIR)/util/stats.h \
$(SRC_DIR)/lp_data/lp_types.h
$(SRC_DIR)/glop/variables_info.h: \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/sparse.h
$(SRC_DIR)/glop/variable_values.h: \
$(SRC_DIR)/glop/basis_representation.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/util/stats.h \
$(SRC_DIR)/lp_data/lp_types.h
$(SRC_DIR)/glop/variables_info.h: \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/sparse.h
$(OBJ_DIR)/glop/basis_representation.$O: \
$(SRC_DIR)/glop/basis_representation.cc \
$(SRC_DIR)/glop/basis_representation.h \
@@ -1013,6 +1013,11 @@ $(OBJ_DIR)/glop/update_row.$O: \
$(SRC_DIR)/lp_data/lp_utils.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/glop/update_row.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Supdate_row.$O
$(OBJ_DIR)/glop/variables_info.$O: \
$(SRC_DIR)/glop/variables_info.cc \
$(SRC_DIR)/glop/variables_info.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/glop/variables_info.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Svariables_info.$O
$(OBJ_DIR)/glop/variable_values.$O: \
$(SRC_DIR)/glop/variable_values.cc \
$(SRC_DIR)/glop/variable_values.h \
@@ -1020,11 +1025,6 @@ $(OBJ_DIR)/glop/variable_values.$O: \
$(SRC_DIR)/lp_data/lp_utils.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/glop/variable_values.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Svariable_values.$O
$(OBJ_DIR)/glop/variables_info.$O: \
$(SRC_DIR)/glop/variables_info.cc \
$(SRC_DIR)/glop/variables_info.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/glop/variables_info.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Svariables_info.$O
$(GEN_DIR)/glop/parameters.pb.cc: $(SRC_DIR)/glop/parameters.proto
$(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) --cpp_out=$(GEN_DIR) $(SRC_DIR)/glop/parameters.proto
@@ -1047,8 +1047,8 @@ GRAPH_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -1265,8 +1265,8 @@ ALGORITHMS_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -1379,8 +1379,8 @@ SAT_DEPS = \
$(GEN_DIR)/sat/boolean_problem.pb.h \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/integer_expr.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
@@ -1396,8 +1396,8 @@ SAT_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -1420,8 +1420,8 @@ SAT_DEPS = \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/matrix_scaler.h \
$(SRC_DIR)/lp_data/permutation.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_column.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_vector.h \
$(SRC_DIR)/glop/basis_representation.h \
$(SRC_DIR)/glop/dual_edge_norms.h \
@@ -1436,8 +1436,8 @@ SAT_DEPS = \
$(SRC_DIR)/glop/revised_simplex.h \
$(SRC_DIR)/glop/status.h \
$(SRC_DIR)/glop/update_row.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/linear_solver/linear_solver.h \
$(GEN_DIR)/linear_solver/linear_solver.pb.h
@@ -1454,6 +1454,7 @@ SAT_LIB_OBJS = \
$(OBJ_DIR)/sat/lp_utils.$O \
$(OBJ_DIR)/sat/no_cycle.$O \
$(OBJ_DIR)/sat/optimization.$O \
$(OBJ_DIR)/sat/overload_checker.$O \
$(OBJ_DIR)/sat/pb_constraint.$O \
$(OBJ_DIR)/sat/precedences.$O \
$(OBJ_DIR)/sat/sat_solver.$O \
@@ -1476,9 +1477,9 @@ $(SRC_DIR)/sat/clause.h: \
$(SRC_DIR)/sat/sat_base.h \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/random.h \
$(SRC_DIR)/base/stringprintf.h \
@@ -1508,6 +1509,12 @@ $(SRC_DIR)/sat/encoding.h: \
$(GEN_DIR)/sat/boolean_problem.pb.h \
$(SRC_DIR)/sat/sat_solver.h
$(SRC_DIR)/sat/integer_expr.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h
$(SRC_DIR)/sat/integer.h: \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h \
@@ -1521,15 +1528,9 @@ $(SRC_DIR)/sat/integer.h: \
$(SRC_DIR)/util/rev.h \
$(SRC_DIR)/util/saturated_arithmetic.h
$(SRC_DIR)/sat/integer_expr.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h
$(SRC_DIR)/sat/intervals.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/integer_expr.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
@@ -1556,6 +1557,13 @@ $(SRC_DIR)/sat/optimization.h: \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_solver.h
$(SRC_DIR)/sat/overload_checker.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h \
$(SRC_DIR)/base/macros.h
$(SRC_DIR)/sat/pb_constraint.h: \
$(SRC_DIR)/sat/sat_base.h \
$(GEN_DIR)/sat/sat_parameters.pb.h \
@@ -1583,9 +1591,9 @@ $(SRC_DIR)/sat/sat_solver.h: \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/base/adjustable_priority_queue.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/map_util.h \
$(SRC_DIR)/base/random.h \
@@ -1707,6 +1715,12 @@ $(OBJ_DIR)/sat/optimization.$O: \
$(SRC_DIR)/sat/util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/optimization.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Soptimization.$O
$(OBJ_DIR)/sat/overload_checker.$O: \
$(SRC_DIR)/sat/overload_checker.cc \
$(SRC_DIR)/sat/overload_checker.h \
$(SRC_DIR)/sat/sat_solver.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/overload_checker.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Soverload_checker.$O
$(OBJ_DIR)/sat/pb_constraint.$O: \
$(SRC_DIR)/sat/pb_constraint.cc \
$(SRC_DIR)/sat/pb_constraint.h \
@@ -1758,6 +1772,7 @@ $(OBJ_DIR)/sat/table.$O: \
$(OBJ_DIR)/sat/timetabling.$O: \
$(SRC_DIR)/sat/timetabling.cc \
$(SRC_DIR)/sat/overload_checker.h \
$(SRC_DIR)/sat/sat_solver.h \
$(SRC_DIR)/sat/timetabling.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/timetabling.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Stimetabling.$O
@@ -1797,8 +1812,8 @@ BOP_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -1813,8 +1828,8 @@ BOP_DEPS = \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/matrix_scaler.h \
$(SRC_DIR)/lp_data/permutation.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_column.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_vector.h \
$(SRC_DIR)/glop/basis_representation.h \
$(SRC_DIR)/glop/dual_edge_norms.h \
@@ -1829,14 +1844,14 @@ BOP_DEPS = \
$(SRC_DIR)/glop/revised_simplex.h \
$(SRC_DIR)/glop/status.h \
$(SRC_DIR)/glop/update_row.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/sat/boolean_problem.h \
$(GEN_DIR)/sat/boolean_problem.pb.h \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/integer_expr.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
@@ -1877,9 +1892,9 @@ $(SRC_DIR)/bop/bop_fs.h: \
$(SRC_DIR)/bop/bop_types.h \
$(SRC_DIR)/bop/bop_util.h \
$(SRC_DIR)/base/basictypes.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/util/time_limit.h \
@@ -1894,9 +1909,9 @@ $(SRC_DIR)/bop/bop_lns.h: \
$(SRC_DIR)/bop/bop_types.h \
$(SRC_DIR)/bop/bop_util.h \
$(SRC_DIR)/base/basictypes.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/util/stats.h \
@@ -1937,9 +1952,9 @@ $(SRC_DIR)/bop/bop_solver.h: \
$(SRC_DIR)/bop/bop_solution.h \
$(SRC_DIR)/bop/bop_types.h \
$(SRC_DIR)/base/basictypes.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/util/stats.h \
@@ -2101,8 +2116,8 @@ LP_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -2117,8 +2132,8 @@ LP_DEPS = \
$(SRC_DIR)/lp_data/lp_types.h \
$(SRC_DIR)/lp_data/matrix_scaler.h \
$(SRC_DIR)/lp_data/permutation.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_column.h \
$(SRC_DIR)/lp_data/sparse.h \
$(SRC_DIR)/lp_data/sparse_vector.h \
$(SRC_DIR)/glop/basis_representation.h \
$(SRC_DIR)/glop/dual_edge_norms.h \
@@ -2133,8 +2148,8 @@ LP_DEPS = \
$(SRC_DIR)/glop/revised_simplex.h \
$(SRC_DIR)/glop/status.h \
$(SRC_DIR)/glop/update_row.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/glop/variables_info.h \
$(SRC_DIR)/glop/variable_values.h \
$(SRC_DIR)/bop/bop_base.h \
$(SRC_DIR)/bop/bop_lns.h \
$(GEN_DIR)/bop/bop_parameters.pb.h \
@@ -2157,14 +2172,6 @@ LP_LIB_OBJS = \
$(OBJ_DIR)/linear_solver/sulum_interface.$O \
$(OBJ_DIR)/linear_solver/linear_solver.pb.$O
$(SRC_DIR)/linear_solver/linear_solver.h: \
$(GEN_DIR)/linear_solver/linear_solver.pb.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/timer.h \
$(GEN_DIR)/glop/parameters.pb.h
$(SRC_DIR)/linear_solver/linear_solver_ext.h: \
$(SRC_DIR)/linear_solver/linear_solver.h \
$(SRC_DIR)/base/commandlineflags.h \
@@ -2176,6 +2183,14 @@ $(SRC_DIR)/linear_solver/linear_solver_ext.h: \
$(SRC_DIR)/base/strutil.h \
$(SRC_DIR)/base/timer.h
$(SRC_DIR)/linear_solver/linear_solver.h: \
$(GEN_DIR)/linear_solver/linear_solver.pb.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/timer.h \
$(GEN_DIR)/glop/parameters.pb.h
$(SRC_DIR)/linear_solver/model_exporter.h: \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/macros.h
@@ -2353,8 +2368,8 @@ CP_DEPS = \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/file.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -2377,8 +2392,8 @@ CP_DEPS = \
$(GEN_DIR)/sat/boolean_problem.pb.h \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/integer_expr.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
@@ -2394,8 +2409,8 @@ CP_LIB_OBJS = \
$(OBJ_DIR)/constraint_solver/alldiff_cst.$O \
$(OBJ_DIR)/constraint_solver/assignment.$O \
$(OBJ_DIR)/constraint_solver/collect_variables.$O \
$(OBJ_DIR)/constraint_solver/constraint_solver.$O \
$(OBJ_DIR)/constraint_solver/constraints.$O \
$(OBJ_DIR)/constraint_solver/constraint_solver.$O \
$(OBJ_DIR)/constraint_solver/count_cst.$O \
$(OBJ_DIR)/constraint_solver/default_search.$O \
$(OBJ_DIR)/constraint_solver/demon_profiler.$O \
@@ -2473,28 +2488,28 @@ $(SRC_DIR)/constraint_solver/constraint_solveri.h: \
$(SRC_DIR)/constraint_solver/hybrid.h: \
$(SRC_DIR)/constraint_solver/constraint_solver.h
$(SRC_DIR)/constraint_solver/routing_flags.h: \
$(GEN_DIR)/constraint_solver/routing_parameters.pb.h \
$(SRC_DIR)/base/commandlineflags.h
$(SRC_DIR)/constraint_solver/routing.h: \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(GEN_DIR)/constraint_solver/routing_parameters.pb.h \
$(SRC_DIR)/base/adjustable_priority_queue-inl.h \
$(SRC_DIR)/base/adjustable_priority_queue.h \
$(SRC_DIR)/base/adjustable_priority_queue-inl.h \
$(SRC_DIR)/base/callback.h \
$(SRC_DIR)/base/commandlineflags.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/util/range_query_function.h \
$(SRC_DIR)/util/sorted_interval_list.h \
$(SRC_DIR)/graph/graph.h
$(SRC_DIR)/constraint_solver/routing_flags.h: \
$(GEN_DIR)/constraint_solver/routing_parameters.pb.h \
$(SRC_DIR)/base/commandlineflags.h
$(SRC_DIR)/constraint_solver/sat_constraint.h: \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
@@ -2507,9 +2522,9 @@ $(OBJ_DIR)/constraint_solver/ac4_mdd_reset_table.$O: \
$(SRC_DIR)/constraint_solver/ac4_mdd_reset_table.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/base/map_util.h \
@@ -2521,9 +2536,9 @@ $(OBJ_DIR)/constraint_solver/ac4r_table.$O: \
$(SRC_DIR)/constraint_solver/ac4r_table.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
$(SRC_DIR)/base/map_util.h \
@@ -2565,6 +2580,16 @@ $(OBJ_DIR)/constraint_solver/collect_variables.$O: \
$(SRC_DIR)/base/stl_util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/constraint_solver/collect_variables.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Scollect_variables.$O
$(OBJ_DIR)/constraint_solver/constraints.$O: \
$(SRC_DIR)/constraint_solver/constraints.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/util/saturated_arithmetic.h \
$(SRC_DIR)/util/string_array.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/constraint_solver/constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Sconstraints.$O
$(OBJ_DIR)/constraint_solver/constraint_solver.$O: \
$(SRC_DIR)/constraint_solver/constraint_solver.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
@@ -2584,16 +2609,6 @@ $(OBJ_DIR)/constraint_solver/constraint_solver.$O: \
$(SRC_DIR)/util/tuple_set.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/constraint_solver/constraint_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Sconstraint_solver.$O
$(OBJ_DIR)/constraint_solver/constraints.$O: \
$(SRC_DIR)/constraint_solver/constraints.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/util/saturated_arithmetic.h \
$(SRC_DIR)/util/string_array.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/constraint_solver/constraints.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Sconstraints.$O
$(OBJ_DIR)/constraint_solver/count_cst.$O: \
$(SRC_DIR)/constraint_solver/count_cst.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
@@ -2649,9 +2664,9 @@ $(OBJ_DIR)/constraint_solver/diffn.$O: \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/hash.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/stringprintf.h \
$(SRC_DIR)/util/string_array.h
@@ -2718,9 +2733,9 @@ $(OBJ_DIR)/constraint_solver/gcc.$O: \
$(SRC_DIR)/constraint_solver/gcc.cc \
$(SRC_DIR)/constraint_solver/constraint_solver.h \
$(SRC_DIR)/constraint_solver/constraint_solveri.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
$(SRC_DIR)/base/integral_types.h \
$(SRC_DIR)/base/join.h \
$(SRC_DIR)/base/logging.h \
$(SRC_DIR)/base/macros.h \
@@ -3093,3 +3108,4 @@ $(GEN_DIR)/constraint_solver/solver_parameters.pb.h: $(GEN_DIR)/constraint_solve
$(OBJ_DIR)/constraint_solver/solver_parameters.pb.$O: $(GEN_DIR)/constraint_solver/solver_parameters.pb.cc
$(CCC) $(CFLAGS) -c $(GEN_DIR)/constraint_solver/solver_parameters.pb.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Ssolver_parameters.pb.$O

19
src/flatzinc/sat_fz_solver.cc
View File

@@ -1088,6 +1088,7 @@ void SolveWithSat(const fz::Model& fz_model, const fz::FlatzincParameters& p,
hash_map<std::pair<int64, int64>, int> num_fully_encoded_vars_per_bounds;
FZLOG << "Extracting " << fz_model.variables().size() << " variables. "
<< FZENDL;
int num_capped_variables = 0;
for (fz::IntegerVariable* var : fz_model.variables()) {
if (!var->active) continue;
@@ -1098,9 +1099,16 @@ void SolveWithSat(const fz::Model& fz_model, const fz::FlatzincParameters& p,
continue;
}
num_vars_per_bounds[{var->domain.Min(), var->domain.Max()}]++;
m.var_map[var] =
m.model.Add(NewIntegerVariable(var->domain.Min(), var->domain.Max()));
const int64 safe_min =
var->domain.Min() == kint64min ? kint32min : var->domain.Min();
const int64 safe_max =
var->domain.Max() == kint64max ? kint32max : var->domain.Max();
if (safe_min != var->domain.Min() || safe_max != var->domain.Max()) {
num_capped_variables++;
}
num_vars_per_bounds[{safe_min, safe_max}]++;
m.var_map[var] = m.model.Add(NewIntegerVariable(safe_min, safe_max));
// We fully encode a variable if it is given as a list of values. Otherwise,
// we will lazily-encode it depending on the constraints it appears in or if
@@ -1125,6 +1133,11 @@ void SolveWithSat(const fz::Model& fz_model, const fz::FlatzincParameters& p,
}
FZLOG << " - " << num_constants << " constants in {"
<< strings::Join(constant_values, ",") << "}." << FZENDL;
if (num_capped_variables > 0) {
FZLOG << " - " << num_capped_variables
<< " variables have been capped to fit into [int32min .. int32max]"
<< FZENDL;
}
// Extract all the constraints.
FZLOG << "Extracting " << fz_model.constraints().size() << " constraints. "

45
src/sat/integer.cc
View File

@@ -776,7 +776,19 @@ GenericLiteralWatcher::GenericLiteralWatcher(
integer_trail_->RegisterWatcher(&modified_vars_);
}
void GenericLiteralWatcher::UpdateCallingNeeds() {
void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) {
// Process any new Literal on the trail.
while (propagation_trail_index_ < trail->Index()) {
const Literal literal = (*trail)[propagation_trail_index_++];
if (literal.Index() >= literal_to_watcher_ids_.size()) continue;
for (const int id : literal_to_watcher_ids_[literal.Index()]) {
if (!in_queue_[id]) {
in_queue_[id] = true;
queue_.push_back(id);
}
}
}
// Process the newly changed variables lower bounds.
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var.value() >= var_to_watcher_ids_.size()) continue;
@@ -790,21 +802,18 @@ void GenericLiteralWatcher::UpdateCallingNeeds() {
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
}
// TODO(user): With the current setup, we will reach a fix-point of all the
// "integer" propagators registered with this class before going back to the SAT
// solver that will propagate its clauses. It may be more efficient to go back
// earlier to the SAT solver, like each time we propagate a literal. This is
// unclear though, so it will require a lot of experiments. Maybe expose the
// various posibilities in the parameters, so that it is easy to try on
// different problems.
bool GenericLiteralWatcher::Propagate(Trail* trail) {
while (propagation_trail_index_ < trail->Index()) {
const Literal literal = (*trail)[propagation_trail_index_++];
if (literal.Index() >= literal_to_watcher_ids_.size()) continue;
for (const int id : literal_to_watcher_ids_[literal.Index()]) {
if (!in_queue_[id]) {
in_queue_[id] = true;
queue_.push_back(id);
}
}
}
const int level = trail->CurrentDecisionLevel();
rev_int_repository_->SetLevel(level);
UpdateCallingNeeds();
UpdateCallingNeeds(trail);
while (!queue_.empty()) {
const int id = queue_.front();
queue_.pop_front();
@@ -831,12 +840,12 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
in_queue_[id] = false;
return false;
}
UpdateCallingNeeds();
// We mark the node afterwards because we assume that the Propagate() method
// is idempotent and never need to be called twice in a row. If some
// propagator don't have this property, we could add an option to call them
// again until nothing changes.
// We mark the node after UpdateCallingNeeds() because we assume that the
// Propagate() method is idempotent and never need to be called twice in a
// row. If some propagator don't have this property, we could add an option
// to call them again until nothing changes.
UpdateCallingNeeds(trail);
in_queue_[id] = false;
}
return true;

2
src/sat/integer.h
View File

@@ -631,7 +631,7 @@ class GenericLiteralWatcher : public SatPropagator {
private:
// Updates queue_ and in_queue_ with the propagator ids that need to be
// called.
void UpdateCallingNeeds();
void UpdateCallingNeeds(Trail* trail);
IntegerTrail* integer_trail_;
RevRepository<int>* rev_int_repository_;

197
src/sat/overload_checker.cc Normal file
View File

@@ -0,0 +1,197 @@
// Copyright 2010-2014 Google
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "sat/overload_checker.h"
//#include "base/iterator_adaptors.h"
#include "sat/sat_solver.h"
namespace operations_research {
namespace sat {
OverloadChecker::OverloadChecker(
const std::vector<IntervalVariable>& interval_vars,
const std::vector<IntegerVariable>& demand_vars, IntegerVariable capacity,
IntegerTrail* integer_trail, IntervalsRepository* intervals_repository)
: num_tasks_(interval_vars.size()),
interval_vars_(interval_vars),
demand_vars_(demand_vars),
capacity_var_(capacity),
integer_trail_(integer_trail),
intervals_repository_(intervals_repository) {
CHECK_GT(num_tasks_, 1);
// Collect the variables.
start_vars_.resize(num_tasks_);
end_vars_.resize(num_tasks_);
duration_vars_.resize(num_tasks_);
for (int t = 0; t < num_tasks_; ++t) {
const IntervalVariable i = interval_vars[t];
start_vars_[t] = intervals_repository->StartVar(i);
end_vars_[t] = intervals_repository->EndVar(i);
duration_vars_[t] = intervals_repository->SizeVar(i);
}
// Allocate space for the sorted tasks.
by_start_min_.reserve(num_tasks_);
by_end_max_.reserve(num_tasks_);
task_to_index_in_start_min_.resize(num_tasks_);
}
void OverloadChecker::ResetThetaTree(int num_tasks) {
// Compute the position of the first and last leaves. The position of the
// first leaf is the smallest power of two that is greater or equal to the
// number of tasks, i.e., the first node of the last level of the tree.
// Remember that the root node starts at position 1.
first_leaf_ = num_tasks - 1;
first_leaf_ |= first_leaf_ >> 16;
first_leaf_ |= first_leaf_ >> 8;
first_leaf_ |= first_leaf_ >> 4;
first_leaf_ |= first_leaf_ >> 2;
first_leaf_ |= first_leaf_ >> 1;
first_leaf_ += 1;
const int last_leaf_ = first_leaf_ + num_tasks - 1;
// Add a dummy leaf to simplify the algorithm if the last leaf is not the
// right child of its parent. Left children are always at an even position.
const int tree_size_ = (last_leaf_ | 1) + 1;
// Reset all the tree nodes.
energies_.assign(tree_size_, IntegerValue(0));
envelopes_.assign(tree_size_, kMinIntegerValue);
leaf_to_task_.resize(num_tasks_);
}
void OverloadChecker::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
watcher->WatchUpperBound(capacity_var_, id);
for (int t = 0; t < num_tasks_; ++t) {
watcher->WatchIntegerVariable(start_vars_[t], id);
watcher->WatchIntegerVariable(end_vars_[t], id);
watcher->WatchLowerBound(demand_vars_[t], id);
if (duration_vars_[t] != kNoIntegerVariable) {
watcher->WatchLowerBound(duration_vars_[t], id);
}
}
}
bool OverloadChecker::Propagate() {
// Sort the tasks by start min and end max.
by_start_min_.clear();
by_end_max_.clear();
for (int t = 0; t < num_tasks_; t++) {
// Tasks with no energy have no impact in the algorithm and are not
// considered in the remainder of this function.
if (DurationMin(t) > 0 && DemandMin(t) > 0) {
by_start_min_.push_back(TaskTime(t, StartMin(t)));
by_end_max_.push_back(TaskTime(t, EndMax(t)));
}
}
std::sort(by_start_min_.begin(), by_start_min_.end());
std::sort(by_end_max_.begin(), by_end_max_.end());
// Link each unskipped task to its position in by_start_min_.
for (int i = 0; i < by_start_min_.size(); ++i) {
task_to_index_in_start_min_[by_start_min_[i].task_id] = i;
}
// Resize the theta-tree and reset all its nodes.
ResetThetaTree(by_start_min_.size());
// Maximum capacity to not exceed.
const IntegerValue capacity_max = integer_trail_->UpperBound(capacity_var_);
// Build the left cuts and check for a possible overload.
for (int i = 0; i < by_end_max_.size(); ++i) {
const int task_id = by_end_max_[i].task_id;
const int leaf_id = task_to_index_in_start_min_[task_id];
// Compute the energy and envelope of the task.
const IntegerValue energy = DurationMin(task_id) * DemandMin(task_id);
const IntegerValue envelope = StartMin(task_id) * capacity_max + energy;
DCHECK_GT(energy, kMinIntegerValue);
DCHECK_GT(envelope, kMinIntegerValue);
// Insert the task in the Theta-tree. This will compute the envelope of the
// left-cut ending with task task_id where the left-cut of task_id is the
// set of all tasks having a maximum ending time that is lower or equal than
// the maximum ending time of task_id.
InsertTaskInThetaTree(task_id, leaf_id, energy, envelope);
// Compute the minimum capacity required to provide the left-cut with enough
// energy. The minimum capacity is ceil(envelopes_[i] / EndMax(task_id)).
IntegerValue new_capacity_min = envelopes_[1] / EndMax(task_id);
if (envelopes_[1] % EndMax(task_id) != 0) new_capacity_min++;
// Do not explain if the minimum capacity does not increase.
if (new_capacity_min <= integer_trail_->LowerBound(capacity_var_)) continue;
reason_.clear();
// Collect the tasks responsible for the value of the envelope.
ExplainEnvelope(1);
// Current capacity of the resource.
reason_.push_back(integer_trail_->UpperBoundAsLiteral(capacity_var_));
// Explain the increase of minimum capacity.
if (!integer_trail_->Enqueue(
IntegerLiteral::GreaterOrEqual(capacity_var_, new_capacity_min),
/*literal_reason=*/{}, reason_)) {
return false;
}
}
return true;
}
void OverloadChecker::InsertTaskInThetaTree(int task_id, int leaf_id,
IntegerValue energy,
IntegerValue envelope) {
const int leaf_node = first_leaf_ + leaf_id;
DCHECK_LT(leaf_node, energies_.size());
leaf_to_task_[leaf_id] = task_id;
energies_[leaf_node] = energy;
envelopes_[leaf_node] = envelope;
int parent = leaf_node / 2;
while (parent != 0) {
DCHECK_LT(parent, first_leaf_);
const int left = parent * 2;
const int right = left + 1;
energies_[parent] = energies_[left] + energies_[right];
envelopes_[parent] =
std::max(envelopes_[left] + energies_[right], envelopes_[right]);
parent = parent / 2;
}
}
void OverloadChecker::ExplainEnvelope(int parent) {
if (parent >= first_leaf_) {
const int t = leaf_to_task_[parent - first_leaf_];
reason_.push_back(integer_trail_->UpperBoundAsLiteral(end_vars_[t]));
reason_.push_back(integer_trail_->LowerBoundAsLiteral(start_vars_[t]));
reason_.push_back(integer_trail_->LowerBoundAsLiteral(demand_vars_[t]));
if (duration_vars_[t] != kNoIntegerVariable) {
reason_.push_back(integer_trail_->LowerBoundAsLiteral(duration_vars_[t]));
}
} else {
const int left = parent * 2;
const int right = left + 1;
if (envelopes_[right] == kMinIntegerValue) {
ExplainEnvelope(left);
} else if (envelopes_[right] == envelopes_[parent]) {
ExplainEnvelope(right);
} else {
ExplainEnvelope(left);
ExplainEnvelope(right);
}
}
}
} // namespace sat
} // namespace operations_research

153
src/sat/overload_checker.h Normal file
View File

@@ -0,0 +1,153 @@
// Copyright 2010-2014 Google
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_SAT_OVERLOAD_CHECKER_H_
#define OR_TOOLS_SAT_OVERLOAD_CHECKER_H_
#include "sat/integer.h"
#include "sat/intervals.h"
#include "sat/model.h"
#include "sat/sat_base.h"
namespace operations_research {
namespace sat {
// Overload Checker
//
// This propagator implements the overload checker filtering rule presented in
// Vilim Petr, "Max Energy Filtering Algorithm for Discrete Cumulative
// Constraint", CPAIOR 2009, http://vilim.eu/petr/cpaior2009.pdf.
//
// This propagator only increases the minimum of the capacity variable or fails
// if the minimum capacity cannot be increased. It has a time complexity of
// O(n log n).
//
// The propagator relies on a Theta-tree to maintain the energy and envelope of
// several set of tasks.
//
// The energy of a task can be seen as its surface and is the product of its
// minimum demand and minimum duration. The energy of a set of tasks is the sum
// of the energy of its tasks.
//
// The envelope of a task is the sum of the task energy and the total amount of
// energy available before the minimum starting time of the task, i.e., the
// product of its minimum start time by the maximum capacity of the resource.
//
// An overload, meaning that there is no solution, occurs when a set of tasks
// requires more energy than what is available between its starting and ending
// times.
//
// Be aware that overload checker is not enough to ensure that the cumulative
// constraint holds. This propagator should thus always be used with a
// timetabling propagator at least.
class OverloadChecker : public PropagatorInterface {
public:
OverloadChecker(const std::vector<IntervalVariable>& interval_vars,
const std::vector<IntegerVariable>& demand_vars,
IntegerVariable capacity, IntegerTrail* integer_trail,
IntervalsRepository* intervals_repository);
bool Propagate() final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
struct TaskTime {
/* const */ int task_id;
/* const */ IntegerValue time;
TaskTime(int task_id, IntegerValue time) : task_id(task_id), time(time) {}
bool operator<(TaskTime other) const { return time < other.time; }
bool operator>(TaskTime other) const { return time > other.time; }
};
// Insert the task task_id to the leaf leaf_id with the given energy and
// envelope. The change is propagated to the top of the Theta-tree by
// recomputing the energy and the envelope of all the leaf's ancestors.
void InsertTaskInThetaTree(int task_id, int leaf_id, IntegerValue energy,
IntegerValue envelope);
// Explores the Theta-tree routed at node parent and explains the value of its
// envelope by filling the reason_ vector. This function does not clear the
// reason_ vector.
void ExplainEnvelope(int parent);
// Reset the theta-tree such that its deepest level is the first that can
// contain at least num_tasks leaves. All nodes are resets to energy = 0 and
// envelope = kMinIntegerValue.
void ResetThetaTree(int num_tasks);
IntegerValue StartMin(int task_id) const {
return integer_trail_->LowerBound(start_vars_[task_id]);
}
IntegerValue EndMax(int task_id) const {
return integer_trail_->UpperBound(end_vars_[task_id]);
}
IntegerValue DemandMin(int task_id) const {
return integer_trail_->LowerBound(demand_vars_[task_id]);
}
IntegerValue DurationMin(int task_id) const {
if (duration_vars_[task_id] != kNoIntegerVariable) {
return integer_trail_->LowerBound(duration_vars_[task_id]);
}
return intervals_repository_->FixedSize(interval_vars_[task_id]);
}
// Number of tasks.
const int num_tasks_;
// IntervalVariable and IntegerVariable of each tasks that must be considered
// by this propagator.
std::vector<IntervalVariable> interval_vars_;
std::vector<IntegerVariable> start_vars_;
std::vector<IntegerVariable> end_vars_;
std::vector<IntegerVariable> demand_vars_;
std::vector<IntegerVariable> duration_vars_;
// Capacity of the resource.
const IntegerVariable capacity_var_;
// Reason vector.
std::vector<IntegerLiteral> reason_;
IntegerTrail* integer_trail_;
IntervalsRepository* intervals_repository_;
std::vector<TaskTime> by_start_min_;
std::vector<TaskTime> by_end_max_;
std::vector<int> task_to_index_in_start_min_;
// The Theta-tree is a complete binary tree that stores the tasks from left to
// right in the leaves of its deepest level. We implement the Theta-tree in a
// vector such that the root node is at position 1. The left and right
// children of a node at position p are respectively stored at positions 2*p
// and 2*p + 1.
// Position of the first leaf.
int first_leaf_;
// Energy of each node in the Theta-tree.
std::vector<IntegerValue> energies_;
// Envelope of each node in the Theta-tree.
std::vector<IntegerValue> envelopes_;
// Tasks of each leaf of the Theta-tree.
std::vector<int> leaf_to_task_;
DISALLOW_COPY_AND_ASSIGN(OverloadChecker);
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_OVERLOAD_CHECKER_H_

10
src/sat/precedences.cc
View File

@@ -238,6 +238,16 @@ void PrecedencesPropagator::AddArc(IntegerVariable tail, IntegerVariable head,
}
}
// Remove the offset_var if it is fixed.
// TODO(user): We should also handle the case where tail or head is fixed.
if (offset_var != kNoIntegerVariable) {
const IntegerValue lb = integer_trail_->LowerBound(offset_var);
if (lb == integer_trail_->UpperBound(offset_var)) {
offset += lb;
offset_var = kNoIntegerVariable;
}
}
AdjustSizeFor(tail);
AdjustSizeFor(head);
if (offset_var != kNoIntegerVariable) AdjustSizeFor(offset_var);

35
src/sat/timetabling.cc
View File

@@ -14,6 +14,7 @@
#include <algorithm>
//#include "base/iterator_adaptors.h"
#include "sat/overload_checker.h"
#include "sat/sat_solver.h"
#include "sat/timetabling.h"
@@ -27,13 +28,21 @@ std::function<void(Model*)> Cumulative(const std::vector<IntervalVariable>& vars
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// Propagator responsible for increasing the min of the start variables,
// decreasing the max of the end variables, and increasing the min of the
// capacity variable.
TimeTablingPerTask* cumulative_start = new TimeTablingPerTask(
// Propagator responsible for applying the Overload Checking filtering rule.
// This propagator increases the minimum of the capacity variable.
OverloadChecker* overload_checker =
new OverloadChecker(vars, demands, capacity, integer_trail, intervals);
overload_checker->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(overload_checker);
// Propagator responsible for applying Timetabling filtering rule. This
// propagator increases the minimum of the start variables, decrease the
// maximum of the end variables, and increasing the minimum of the capacity
// variable.
TimeTablingPerTask* time_tabling = new TimeTablingPerTask(
vars, demands, capacity, integer_trail, intervals);
cumulative_start->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(cumulative_start);
time_tabling->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(time_tabling);
};
}
@@ -74,14 +83,12 @@ TimeTablingPerTask::TimeTablingPerTask(
void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
watcher->WatchUpperBound(capacity_var_, id);
for (int i = 0; i < num_tasks_; i++) {
watcher->WatchIntegerVariable(start_vars_[i], id);
watcher->WatchIntegerVariable(end_vars_[i], id);
watcher->WatchLowerBound(demand_vars_[i], id);
const IntegerVariable duration_var =
intervals_repository_->SizeVar(interval_vars_[i]);
if (duration_var != kNoIntegerVariable) {
watcher->WatchLowerBound(duration_var, id);
for (int t = 0; t < num_tasks_; t++) {
watcher->WatchIntegerVariable(start_vars_[t], id);
watcher->WatchIntegerVariable(end_vars_[t], id);
watcher->WatchLowerBound(demand_vars_[t], id);
if (duration_vars_[t] != kNoIntegerVariable) {
watcher->WatchLowerBound(duration_vars_[t], id);
}
}
}