diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk
index 901773a861..f207f5b443 100644
--- a/makefiles/Makefile.gen.mk
+++ b/makefiles/Makefile.gen.mk
@@ -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
+
diff --git a/src/flatzinc/sat_fz_solver.cc b/src/flatzinc/sat_fz_solver.cc
index a82fe5546c..5579a0439c 100644
--- a/src/flatzinc/sat_fz_solver.cc
+++ b/src/flatzinc/sat_fz_solver.cc
@@ -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. "
diff --git a/src/sat/integer.cc b/src/sat/integer.cc
index 098d3821ca..1d941379aa 100644
--- a/src/sat/integer.cc
+++ b/src/sat/integer.cc
@@ -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;
diff --git a/src/sat/integer.h b/src/sat/integer.h
index 258d91e6c4..9c5a460b0d 100644
--- a/src/sat/integer.h
+++ b/src/sat/integer.h
@@ -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_;
diff --git a/src/sat/overload_checker.cc b/src/sat/overload_checker.cc
new file mode 100644
index 0000000000..29d5083a86
--- /dev/null
+++ b/src/sat/overload_checker.cc
@@ -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
diff --git a/src/sat/overload_checker.h b/src/sat/overload_checker.h
new file mode 100644
index 0000000000..1ae17da873
--- /dev/null
+++ b/src/sat/overload_checker.h
@@ -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_
diff --git a/src/sat/precedences.cc b/src/sat/precedences.cc
index f72334a35f..2576286900 100644
--- a/src/sat/precedences.cc
+++ b/src/sat/precedences.cc
@@ -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);
diff --git a/src/sat/timetabling.cc b/src/sat/timetabling.cc
index 64c16ef9c0..2bb7cf1428 100644
--- a/src/sat/timetabling.cc
+++ b/src/sat/timetabling.cc
@@ -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);
     }
   }
 }