diff --git a/.gitignore b/.gitignore index b3e4739ce6..8afdec2b2e 100644 --- a/.gitignore +++ b/.gitignore @@ -27,8 +27,9 @@ lib/ examples/csharp/solution/*.csproj examples/csharp/*.sln -src/bazel-* +ortools/bazel-* examples/bazel-* +bazel-* tools/docker/export diff --git a/examples/python/hidato_sat.py b/examples/python/hidato_sat.py new file mode 100644 index 0000000000..119848b9c4 --- /dev/null +++ b/examples/python/hidato_sat.py @@ -0,0 +1,172 @@ +from ortools.sat.python import cp_model + + +def BuildPairs(rows, cols): + """Build closeness pairs for consecutive numbers. + + Build set of allowed pairs such that two consecutive numbers touch + each other in the grid. + + Returns: + A list of pairs for allowed consecutive position of numbers. + + Args: + rows: the number of rows in the grid + cols: the number of columns in the grid + """ + return [(x * cols + y, (x + dx) * cols + (y + dy)) + for x in range(rows) for y in range(cols) + for dx in (-1, 0, 1) for dy in (-1, 0, 1) + if (x + dx >= 0 and x + dx < rows and + y + dy >= 0 and y + dy < cols and (dx != 0 or dy != 0))] + + +def PrintSolution(positions, rows, cols): + """Print a current solution.""" + # Create empty board. + board = [] + for _ in range(rows): + board.append([0] * cols) + # Fill board with solution value. + for k in range(rows * cols): + position = positions[k] + board[position // cols][position % cols] = k + 1 + # Print the board. + print('Solution') + PrintMatrix(board) + + +def PrintMatrix(game): + """Pretty print of a matrix.""" + rows = len(game) + cols = len(game[0]) + for i in range(rows): + line = '' + for j in range(cols): + if game[i][j] == 0: + line += ' .' + else: + line += '% 3s' % game[i][j] + print(line) + + +def SolveHidato(problem): + """Solve the given hidato table.""" + # Create the model. + model = cp_model.CpModel() + + # + # models, a 0 indicates an open cell which number is not yet known. + # + # + puzzle = None + if problem == 1: + # Simple problem + puzzle = [[6, 0, 9], + [0, 2, 8], + [1, 0, 0]] + + elif problem == 2: + puzzle = [[0, 44, 41, 0, 0, 0, 0], + [0, 43, 0, 28, 29, 0, 0], + [0, 1, 0, 0, 0, 33, 0], + [0, 2, 25, 4, 34, 0, 36], + [49, 16, 0, 23, 0, 0, 0], + [0, 19, 0, 0, 12, 7, 0], + [0, 0, 0, 14, 0, 0, 0]] + + elif problem == 3: + # Problems from the book: + # Gyora Bededek: "Hidato: 2000 Pure Logic Puzzles" + # Problem 1 (Practice) + puzzle = [[0, 0, 20, 0, 0], + [0, 0, 0, 16, 18], + [22, 0, 15, 0, 0], + [23, 0, 1, 14, 11], + [0, 25, 0, 0, 12]] + + elif problem == 4: + # problem 2 (Practice) + puzzle = [[0, 0, 0, 0, 14], + [0, 18, 12, 0, 0], + [0, 0, 17, 4, 5], + [0, 0, 7, 0, 0], + [9, 8, 25, 1, 0]] + + elif problem == 5: + # problem 3 (Beginner) + puzzle = [[0, 26, 0, 0, 0, 18], + [0, 0, 27, 0, 0, 19], + [31, 23, 0, 0, 14, 0], + [0, 33, 8, 0, 15, 1], + [0, 0, 0, 5, 0, 0], + [35, 36, 0, 10, 0, 0]] + elif problem == 6: + # Problem 15 (Intermediate) + puzzle = [[64, 0, 0, 0, 0, 0, 0, 0], + [1, 63, 0, 59, 15, 57, 53, 0], + [0, 4, 0, 14, 0, 0, 0, 0], + [3, 0, 11, 0, 20, 19, 0, 50], + [0, 0, 0, 0, 22, 0, 48, 40], + [9, 0, 0, 32, 23, 0, 0, 41], + [27, 0, 0, 0, 36, 0, 46, 0], + [28, 30, 0, 35, 0, 0, 0, 0]] + + r = len(puzzle) + c = len(puzzle[0]) + + print(('Initial game (%i x %i)' % (r, c))) + PrintMatrix(puzzle) + + # + # declare variables + # + positions = [model.NewIntVar(0, r * c - 1, 'p[%i]' % i) + for i in range(r * c)] + + # + # constraints + # + model.AddAllDifferent(positions) + + # + # Fill in the clues + # + for i in range(r): + for j in range(c): + if puzzle[i][j] > 0: + model.Add(positions[puzzle[i][j] - 1] == i * c + j) + + # Consecutive numbers much touch each other in the grid. + # We use an allowed assignment constraint to model it. + close_tuples = BuildPairs(r, c) + for k in range(0, r * c - 1): + model.AddAllowedAssignments([positions[k], positions[k + 1]], close_tuples) + + # + # solution and search + # + + solver = cp_model.CpSolver() + status = solver.Solve(model) + + if status == cp_model.MODEL_SAT: + PrintSolution([solver.Value(x) for x in positions], r, c,) + + print('Statistics') + print(' - conflicts : %i' % solver.NumConflicts()) + print(' - branches : %i' % solver.NumBranches()) + print(' - wall time : %f ms' % solver.WallTime()) + + + +def main(): + for table in range(1, 7): + print('') + print('----- Solving problem %i -----' % table) + print('') + SolveHidato(table) + + +if __name__ == '__main__': + main() diff --git a/examples/python/jobshop_ft06_sat.py b/examples/python/jobshop_ft06_sat.py new file mode 100644 index 0000000000..2f12259f00 --- /dev/null +++ b/examples/python/jobshop_ft06_sat.py @@ -0,0 +1,70 @@ +from ortools.sat.python import cp_model + + +def main(): + # Creates the solver. + model = cp_model.CpModel() + + machines_count = 6 + jobs_count = 6 + all_machines = range(0, machines_count) + all_jobs = range(0, jobs_count) + + durations = [[1, 3, 6, 7, 3, 6], + [8, 5, 10, 10, 10, 4], + [5, 4, 8, 9, 1, 7], + [5, 5, 5, 3, 8, 9], + [9, 3, 5, 4, 3, 1], + [3, 3, 9, 10, 4, 1]] + + machines = [[2, 0, 1, 3, 5, 4], + [1, 2, 4, 5, 0, 3], + [2, 3, 5, 0, 1, 4], + [1, 0, 2, 3, 4, 5], + [2, 1, 4, 5, 0, 3], + [1, 3, 5, 0, 4, 2]] + + # Computes horizon dynamically. + horizon = sum([sum(durations[i]) for i in all_jobs]) + + # Creates jobs. + all_tasks = {} + for i in all_jobs: + for j in all_machines: + start = model.NewIntVar(0, horizon, 'start_%i_%i' % (i, j)) + duration = durations[i][j] + end = model.NewIntVar(0, horizon, 'end_%i_%i' % (i, j)) + interval = model.NewIntervalVar(start, duration, end, + 'interval_%i_%i' % (i, j)) + all_tasks[(i, j)] = (start, end, interval) + + # Create disjuctive constraints. + machine_to_jobs = {} + for i in all_machines: + machines_jobs = [] + for j in all_jobs: + for k in all_machines: + if machines[j][k] == i: + machines_jobs.append(all_tasks[(j, k)][2]) + machine_to_jobs[i] = machines_jobs + model.AddNoOverlap(machines_jobs) + + # Precedences inside a job. + for i in all_jobs: + for j in range(0, machines_count - 1): + model.Add(all_tasks[(i, j + 1)][0] >= all_tasks[(i, j)][1]) + + # Makespan objective. + obj_var = model.NewIntVar(0, horizon, 'makespan') + model.AddMaxEquality( + obj_var, [all_tasks[(i, machines_count - 1)][1] for i in all_jobs]) + model.Minimize(obj_var) + + # Solve model. + solver = cp_model.CpSolver() + response = solver.Solve(model) + print(solver.ObjectiveValue()) + + +if __name__ == '__main__': + main() diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 2e919c4e80..552464417d 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1917,14 +1917,8 @@ IntegerVariable AddLPConstraints(const CpModelProto& model_proto, } } - IntegerVariable main_objective_var; - if (m->GetOrCreate()->parameters().optimize_with_core()) { - main_objective_var = - GetOrCreateVariableWithTightBound(top_level_cp_terms, m->model()); - } else { - main_objective_var = GetOrCreateVariableGreaterOrEqualToSumOf( - top_level_cp_terms, m->model()); - } + const IntegerVariable main_objective_var = + GetOrCreateVariableGreaterOrEqualToSumOf(top_level_cp_terms, m->model()); // Register LP constraints. Note that this needs to be done after all the // constraints have been added. @@ -2085,12 +2079,7 @@ CpSolverResponse SolveCpModelInternal( for (int i = 0; i < obj.vars_size(); ++i) { terms.push_back(std::make_pair(m.Integer(obj.vars(i)), obj.coeffs(i))); } - if (parameters.optimize_with_core()) { - objective_var = GetOrCreateVariableWithTightBound(terms, m.model()); - } else { - objective_var = - GetOrCreateVariableGreaterOrEqualToSumOf(terms, m.model()); - } + objective_var = GetOrCreateVariableGreaterOrEqualToSumOf(terms, m.model()); } // Intersect the objective domain with the given one if any. @@ -2112,7 +2101,7 @@ CpSolverResponse SolveCpModelInternal( // Make sure the sum take a value inside the objective domain by adding // the other side: objective <= sum terms. // - // TODO(user): Use a better condidtion to detect when this is not usefull. + // TODO(user): Use a better condition to detect when this is not usefull. if (user_domain != automatic_domain) { std::vector vars; std::vector coeffs; diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 03794f0e39..bea2f77f4f 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -277,8 +277,11 @@ bool LinearProgrammingConstraint::Propagate() { // it past our current objective upper-bound (we will already fail as soon // as we pass it). Note that this limit is properly transformed using the // objective scaling factor and offset stored in lp_data_. + // + // Note that we use a bigger epsilon here to be sure that if we abort + // because of this, we will report a conflict. parameters.set_objective_upper_limit(static_cast( - integer_trail_->UpperBound(objective_cp_).value() + kEpsilon)); + integer_trail_->UpperBound(objective_cp_).value() + 100.0 * kEpsilon)); } // Put an iteration limit on the work we do in the simplex for this call. Note diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 6f405c32cb..18be30faea 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -34,6 +34,13 @@ from ortools.sat import pywrapsat INT_MIN = -9223372036854775808 # hardcoded to be platform independent. INT_MAX = 9223372036854775807 +# Cp Solver status (exported to avoid importing cp_model_cp2). +UNKNOWN = cp_model_pb2.UNKNOWN +MODEL_INVALID = cp_model_pb2.MODEL_INVALID +MODEL_SAT = cp_model_pb2.MODEL_SAT +MODEL_UNSAT = cp_model_pb2.MODEL_UNSAT +OPTIMAL = cp_model_pb2.OPTIMAL + def AssertIsInt64(x): if not isinstance(x, numbers.Integral): @@ -868,3 +875,15 @@ class CpSolver(object): def StatusName(self, status): return cp_model_pb2.CpSolverStatus.Name(status) + + def NumBooleans(self): + return self.__solution.num_booleans + + def NumConflicts(self): + return self.__solution.num_conflicts + + def NumBranches(self): + return self.__solution.num_branches + + def WallTime(self): + return self.__solution.wall_time diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc index 3f37d176d2..db893917b3 100644 --- a/ortools/sat/table.cc +++ b/ortools/sat/table.cc @@ -89,9 +89,13 @@ void ProcessOneColumn(const std::vector& line_literals, // is false too (i.e not possible). for (int i = 0; i < values.size(); ++i) { const IntegerValue v = values[i]; - value_to_list_of_line_literals[v].push_back(line_literals[i]); - model->Add(Implication(FindOrDie(encoding, v).Negated(), - line_literals[i].Negated())); + if (!ContainsKey(encoding, v)) { + model->Add(ClauseConstraint({line_literals[i].Negated()})); + } else { + value_to_list_of_line_literals[v].push_back(line_literals[i]); + model->Add(Implication(FindOrDie(encoding, v).Negated(), + line_literals[i].Negated())); + } } // If all the tuples containing a value are false, then this value must be @@ -159,7 +163,6 @@ std::function TableConstraint( // Fully encode the variables using all the values appearing in the tuples. IntegerTrail* interger_trail = model->GetOrCreate(); - std::unordered_map encoding; const std::vector> tr_tuples = Transpose(new_tuples); for (int i = 0; i < n; ++i) { const int64 first = tr_tuples[i].front(); @@ -170,11 +173,10 @@ std::function TableConstraint( interger_trail->UpdateInitialDomain( vars[i], SortedDisjointIntervalsFromValues(tr_tuples[i])); model->Add(FullyEncodeVariable(vars[i])); - encoding = GetEncoding(vars[i], model); ProcessOneColumn( tuple_literals, std::vector(tr_tuples[i].begin(), tr_tuples[i].end()), - encoding, model); + GetEncoding(vars[i], model), model); } } }; @@ -223,7 +225,6 @@ std::function NegatedTableConstraintWithoutFullEncoding( const int64 value = tuple[i]; const int64 lb = model->Get(LowerBound(vars[i])); const int64 ub = model->Get(UpperBound(vars[i])); - CHECK_LT(lb, ub); // TODO(user): test the full initial domain instead of just checking // the bounds. if (value < lb || value > ub) { diff --git a/tools/docker/Makefile b/tools/docker/Makefile index 6ca040827f..3c4e3dfcf2 100644 --- a/tools/docker/Makefile +++ b/tools/docker/Makefile @@ -56,6 +56,9 @@ ubuntu-14.04-archive: export ubuntu-14.04-image ubuntu-14.04-test: export ubuntu-14.04-image docker run -w /root/or-tools -v `pwd`/export:/export or-tools-ubuntu-14.04-image:latest /bin/bash -c "git pull; make clean; make all -j 5; make test" +ubuntu-14.04-bash: export ubuntu-14.04-image + docker run -it or-tools-ubuntu-14.04-image:latest /bin/bash + # Ubuntu 16.06 images ubuntu-16.04-image: @@ -70,6 +73,9 @@ ubuntu-16.04-archive: export ubuntu-16.04-image ubuntu-16.04-test: export ubuntu-16.04-image docker run -w /root/or-tools -v `pwd`/export:/export or-tools-ubuntu-16.04-image:latest /bin/bash -c "git pull; make clean; make all -j 5; make test" +ubuntu-16.04-bash: export ubuntu-16.04-image + docker run -it or-tools-ubuntu-16.04-image:latest /bin/bash + # Ubuntu 17.04 images ubuntu-17.04-image: