From efd16c78daefdfd2c1295fb0580cf2acdcfce268 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 3 May 2021 12:11:39 +0200 Subject: [PATCH] [CP-SAT] deprecate SearchAllSolutions and SolveWithSolutionCallback --- .../scheduling_with_transitions_sat.py | 2 +- examples/contrib/school_scheduling_sat.py | 2 +- examples/contrib/stable_marriage_sat.py | 3 +- examples/dotnet/BalanceGroupSat.cs | 2 +- examples/dotnet/NetworkRoutingSat.cs | 8 +-- examples/dotnet/NursesSat.cs | 3 +- examples/python/appointments.py | 6 ++- examples/python/balance_group_sat.py | 2 +- examples/python/flexible_job_shop_sat.py | 3 +- examples/python/gate_scheduling_sat.py | 1 + examples/python/golomb8.py | 1 + examples/python/hidato_sat.py | 1 + examples/python/integer_programming.py | 1 + examples/python/jobshop_ft06_distance_sat.py | 1 + examples/python/jobshop_ft06_sat.py | 1 + .../python/jobshop_with_maintenance_sat.py | 3 +- examples/python/linear_assignment_api.py | 1 + examples/python/linear_programming.py | 1 + examples/python/magic_sequence_distribute.py | 1 + examples/python/nqueens_sat.py | 3 +- examples/python/pyflow_example.py | 1 + examples/python/rcpsp_sat.py | 1 + examples/python/shift_scheduling_sat.py | 3 +- ...duling_with_setup_release_due_dates_sat.py | 2 +- examples/python/steel_mill_slab_sat.py | 7 +-- examples/python/sudoku_sat.py | 1 + .../tasks_and_workers_assignment_sat.py | 2 +- examples/python/vendor_scheduling_sat.py | 3 +- examples/python/wedding_optimal_chart_sat.py | 2 +- examples/python/zebra_sat.py | 1 + examples/tests/cp_model_test.py | 3 +- ortools/sat/cp_model.proto | 5 ++ ortools/sat/cp_model_checker.cc | 16 +++++- ortools/sat/cp_model_search.cc | 5 +- ortools/sat/cp_model_search.h | 1 + ortools/sat/cp_model_solver.cc | 9 ++-- ortools/sat/csharp/CpSolver.cs | 16 +++--- ortools/sat/doc/boolean_logic.md | 3 +- ortools/sat/doc/channeling.md | 13 +++-- ortools/sat/doc/integer_arithmetic.md | 26 +++++++--- ortools/sat/doc/model.md | 6 +-- ortools/sat/doc/scheduling.md | 4 +- ortools/sat/doc/solver.md | 51 +++++++++++++++---- ortools/sat/linear_programming_constraint.cc | 4 +- ortools/sat/python/cp_model.py | 4 +- ortools/sat/samples/ChannelingSampleSat.cs | 5 +- ortools/sat/samples/ChannelingSampleSat.java | 4 +- ortools/sat/samples/CpIsFunSat.cs | 5 +- ortools/sat/samples/CpIsFunSat.java | 5 +- .../EarlinessTardinessCostSampleSat.cs | 5 +- .../EarlinessTardinessCostSampleSat.java | 4 +- .../samples/SearchForAllSolutionsSampleSat.cs | 5 +- .../SearchForAllSolutionsSampleSat.java | 5 +- .../sat/samples/SolutionHintingSampleSat.cs | 2 +- .../sat/samples/SolutionHintingSampleSat.java | 2 +- ...eAndPrintIntermediateSolutionsSampleSat.cs | 2 +- ...ndPrintIntermediateSolutionsSampleSat.java | 2 +- ortools/sat/samples/StepFunctionSampleSat.cs | 5 +- .../sat/samples/StepFunctionSampleSat.java | 4 +- .../samples/StopAfterNSolutionsSampleSat.cs | 3 +- .../samples/StopAfterNSolutionsSampleSat.java | 5 +- .../sat/samples/boolean_product_sample_sat.py | 3 +- ortools/sat/samples/channeling_sample_sat.py | 4 +- ortools/sat/samples/cp_is_fun_sat.py | 5 +- .../earliness_tardiness_cost_sample_sat.py | 4 +- ortools/sat/samples/nurses_sat.py | 4 +- .../scheduling_with_calendar_sample_sat.py | 4 +- .../search_for_all_solutions_sample_sat.py | 5 +- .../samples/solution_hinting_sample_sat.py | 2 +- ...print_intermediate_solutions_sample_sat.py | 2 +- .../sat/samples/step_function_sample_sat.py | 4 +- .../stop_after_n_solutions_sample_sat.py | 5 +- 72 files changed, 241 insertions(+), 99 deletions(-) diff --git a/examples/contrib/scheduling_with_transitions_sat.py b/examples/contrib/scheduling_with_transitions_sat.py index e173ecfe37..cfe7bef613 100644 --- a/examples/contrib/scheduling_with_transitions_sat.py +++ b/examples/contrib/scheduling_with_transitions_sat.py @@ -297,7 +297,7 @@ def main(args): if parameters: text_format.Merge(parameters, solver.parameters) solution_printer = SolutionPrinter(makespan) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) #---------------------------------------------------------------------------- # Print solution. diff --git a/examples/contrib/school_scheduling_sat.py b/examples/contrib/school_scheduling_sat.py index 4f16cdff26..6f29e8c8fe 100644 --- a/examples/contrib/school_scheduling_sat.py +++ b/examples/contrib/school_scheduling_sat.py @@ -117,7 +117,7 @@ class SchoolSchedulingSatSolver(object): print('Solving') solver = cp_model.CpSolver() solution_printer = SchoolSchedulingSatSolutionPrinter() - status = solver.Solve(self.model) + status = solver.Solve(self.model, solution_printer) print() print('status', status) print('Branches', solver.NumBranches()) diff --git a/examples/contrib/stable_marriage_sat.py b/examples/contrib/stable_marriage_sat.py index 905f01225e..59742fdae0 100644 --- a/examples/contrib/stable_marriage_sat.py +++ b/examples/contrib/stable_marriage_sat.py @@ -94,7 +94,8 @@ def main(ranks, pair_num): solver = cp_model.CpSolver() solution_printer = SolutionPrinter(wife, husband) - solver.SearchForAllSolutions(model, solution_printer) + solver.parameters.enumerate_all_solutions = True + solver.Solve(model, solution_printer) if __name__ == "__main__": diff --git a/examples/dotnet/BalanceGroupSat.cs b/examples/dotnet/BalanceGroupSat.cs index 6ac62ec97e..3d2c5071b9 100644 --- a/examples/dotnet/BalanceGroupSat.cs +++ b/examples/dotnet/BalanceGroupSat.cs @@ -147,7 +147,7 @@ public class BalanceGroupSat var solutionPrinter = new SolutionPrinter(values, colors, allGroups, allItems, itemInGroup); - var status = solver.SolveWithSolutionCallback(model, solutionPrinter); + var status = solver.Solve(model, solutionPrinter); } public class SolutionPrinter : CpSolverSolutionCallback diff --git a/examples/dotnet/NetworkRoutingSat.cs b/examples/dotnet/NetworkRoutingSat.cs index bf87d61d66..110ab3f44c 100644 --- a/examples/dotnet/NetworkRoutingSat.cs +++ b/examples/dotnet/NetworkRoutingSat.cs @@ -498,10 +498,11 @@ public class NetworkRoutingSat cpModel.AddAllDifferent(nodeVars); var solver = new CpSolver(); + solver.StringParameters = "enumerate_all_solutions:true"; var solutionPrinter = new FeasibleSolutionChecker(demandIndex, ref _allPaths, maxLength, arcVars, maxPaths, nodeVars); - var status = solver.SearchAllSolutions(cpModel, solutionPrinter); + var status = solver.Solve(cpModel, solutionPrinter); } private long[,] getArcsData() @@ -765,9 +766,10 @@ public class NetworkRoutingSat cpModel.Minimize(LinearExpr.Sum(obj)); CpSolver solver = new CpSolver(); - solver.StringParameters = parameters; + solver.StringParameters = + parameters + " enumerate_all_solutions:true"; - CpSolverStatus status = solver.SearchAllSolutions( + CpSolverStatus status = solver.Solve( cpModel, new FeasibleSolutionChecker2(maxUsageCost, comfortableTrafficVars, trafficVars)); return (long)solver.ObjectiveValue; diff --git a/examples/dotnet/NursesSat.cs b/examples/dotnet/NursesSat.cs index 76a5f69ef6..bf361294c3 100644 --- a/examples/dotnet/NursesSat.cs +++ b/examples/dotnet/NursesSat.cs @@ -195,7 +195,8 @@ public class NursesSat to_print.Add(5091); to_print.Add(7003); NurseSolutionObserver cb = new NurseSolutionObserver(shift, num_nurses, num_days, num_shifts, to_print); - CpSolverStatus status = solver.SearchAllSolutions(model, cb); + solver.StringParameters = "enumerate_all_solutions:true"; + CpSolverStatus status = solver.Solve(model, cb); // Statistics. Console.WriteLine("Statistics"); diff --git a/examples/python/appointments.py b/examples/python/appointments.py index f65f469b99..0862205145 100644 --- a/examples/python/appointments.py +++ b/examples/python/appointments.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. @@ -73,7 +74,10 @@ def EnumerateAllKnapsacksWithRepetition(item_sizes, total_size_min, solver = cp_model.CpSolver() solution_collector = AllSolutionCollector(variables) - solver.SearchForAllSolutions(model, solution_collector) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve + solver.Solve(model, solution_collector) return solution_collector.combinations() diff --git a/examples/python/balance_group_sat.py b/examples/python/balance_group_sat.py index 8e4f8960aa..606852222d 100644 --- a/examples/python/balance_group_sat.py +++ b/examples/python/balance_group_sat.py @@ -163,7 +163,7 @@ def main(): solver = cp_model.CpSolver() solution_printer = SolutionPrinter(values, colors, all_groups, all_items, item_in_group) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) if status == cp_model.OPTIMAL: print('Optimal epsilon: %i' % solver.ObjectiveValue()) diff --git a/examples/python/flexible_job_shop_sat.py b/examples/python/flexible_job_shop_sat.py index 41e16d9d7b..f7c8df4f8c 100644 --- a/examples/python/flexible_job_shop_sat.py +++ b/examples/python/flexible_job_shop_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. @@ -172,7 +173,7 @@ def flexible_jobshop(): # Solve model. solver = cp_model.CpSolver() solution_printer = SolutionPrinter() - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) # Print final solution. for job_id in all_jobs: diff --git a/examples/python/gate_scheduling_sat.py b/examples/python/gate_scheduling_sat.py index 6f26c4184c..4860789f5e 100644 --- a/examples/python/gate_scheduling_sat.py +++ b/examples/python/gate_scheduling_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/golomb8.py b/examples/python/golomb8.py index 52ed20a79d..9525d7c4a0 100644 --- a/examples/python/golomb8.py +++ b/examples/python/golomb8.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/hidato_sat.py b/examples/python/hidato_sat.py index 08a853a6aa..65d654802a 100644 --- a/examples/python/hidato_sat.py +++ b/examples/python/hidato_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/integer_programming.py b/examples/python/integer_programming.py index 1792cc48d0..cbc5d35537 100644 --- a/examples/python/integer_programming.py +++ b/examples/python/integer_programming.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/jobshop_ft06_distance_sat.py b/examples/python/jobshop_ft06_distance_sat.py index c6dfb878ff..a246ab33ce 100644 --- a/examples/python/jobshop_ft06_distance_sat.py +++ b/examples/python/jobshop_ft06_distance_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/jobshop_ft06_sat.py b/examples/python/jobshop_ft06_sat.py index 3b9ea03065..7055ac446e 100644 --- a/examples/python/jobshop_ft06_sat.py +++ b/examples/python/jobshop_ft06_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/jobshop_with_maintenance_sat.py b/examples/python/jobshop_with_maintenance_sat.py index 47b2612ef7..d20211211e 100644 --- a/examples/python/jobshop_with_maintenance_sat.py +++ b/examples/python/jobshop_with_maintenance_sat.py @@ -95,8 +95,7 @@ def jobshop_with_maintenance(): # Solve model. solver = cp_model.CpSolver() solution_printer = SolutionPrinter() - status = solver.SolveWithSolutionCallback(model, solution_printer) - #status = solver.Solve(model) + status = solver.Solve(model, solution_printer) # Output solution. if status == cp_model.OPTIMAL: diff --git a/examples/python/linear_assignment_api.py b/examples/python/linear_assignment_api.py index 3b8241257b..84fc8836b8 100644 --- a/examples/python/linear_assignment_api.py +++ b/examples/python/linear_assignment_api.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/linear_programming.py b/examples/python/linear_programming.py index 830b765a5a..0000921aa6 100644 --- a/examples/python/linear_programming.py +++ b/examples/python/linear_programming.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/magic_sequence_distribute.py b/examples/python/magic_sequence_distribute.py index 3ca5a26633..24897aa3ef 100644 --- a/examples/python/magic_sequence_distribute.py +++ b/examples/python/magic_sequence_distribute.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/nqueens_sat.py b/examples/python/nqueens_sat.py index a5092d57b8..f99b524d5d 100644 --- a/examples/python/nqueens_sat.py +++ b/examples/python/nqueens_sat.py @@ -78,7 +78,8 @@ def main(board_size): ### Solve model. solver = cp_model.CpSolver() solution_printer = NQueenSolutionPrinter(queens) - status = solver.SearchForAllSolutions(model, solution_printer) + solver.parameters.enumerate_all_solutions = True + status = solver.Solve(model, solution_printer) print() print('Statistics') diff --git a/examples/python/pyflow_example.py b/examples/python/pyflow_example.py index 8c3466f29a..11e3c80c48 100644 --- a/examples/python/pyflow_example.py +++ b/examples/python/pyflow_example.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/rcpsp_sat.py b/examples/python/rcpsp_sat.py index 1c6f18001d..f8e3acb972 100644 --- a/examples/python/rcpsp_sat.py +++ b/examples/python/rcpsp_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/shift_scheduling_sat.py b/examples/python/shift_scheduling_sat.py index f7c09f70be..2631adbed2 100644 --- a/examples/python/shift_scheduling_sat.py +++ b/examples/python/shift_scheduling_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. @@ -378,7 +379,7 @@ def solve_shift_scheduling(params, output_proto): if params: text_format.Parse(params, solver.parameters) solution_printer = cp_model.ObjectiveSolutionPrinter() - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) # Print solution. if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE: diff --git a/examples/python/single_machine_scheduling_with_setup_release_due_dates_sat.py b/examples/python/single_machine_scheduling_with_setup_release_due_dates_sat.py index 10c975f9f0..75e5d2d17b 100644 --- a/examples/python/single_machine_scheduling_with_setup_release_due_dates_sat.py +++ b/examples/python/single_machine_scheduling_with_setup_release_due_dates_sat.py @@ -263,7 +263,7 @@ def main(args): if parameters: text_format.Merge(parameters, solver.parameters) solution_printer = SolutionPrinter() - solver.SolveWithSolutionCallback(model, solution_printer) + solver.Solve(model, solution_printer) print(solver.ResponseStats()) for job_id in all_jobs: print('job %i starts at %i end ends at %i' % diff --git a/examples/python/steel_mill_slab_sat.py b/examples/python/steel_mill_slab_sat.py index aa6aacb9be..0d1457e493 100644 --- a/examples/python/steel_mill_slab_sat.py +++ b/examples/python/steel_mill_slab_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. @@ -423,7 +424,7 @@ def steel_mill_slab(problem, break_symmetries): solver = cp_model.CpSolver() solver.parameters.num_search_workers = 8 objective_printer = cp_model.ObjectiveSolutionPrinter() - status = solver.SolveWithSolutionCallback(model, objective_printer) + status = solver.Solve(model, objective_printer) ### Output the solution. if status in (cp_model.OPTIMAL, cp_model.FEASIBLE): @@ -593,7 +594,7 @@ def steel_mill_slab_with_valid_slabs(problem, break_symmetries): solver.num_search_workers = 8 solution_printer = SteelMillSlabSolutionPrinter(orders, assign, loads, losses) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) ### Output the solution. if status == cp_model.OPTIMAL: @@ -661,7 +662,7 @@ def steel_mill_slab_with_column_generation(problem): solver.parameters.num_search_workers = 8 solver.parameters.log_search_progress = True solution_printer = cp_model.ObjectiveSolutionPrinter() - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) ### Output the solution. if status in (cp_model.OPTIMAL, cp_model.FEASIBLE): diff --git a/examples/python/sudoku_sat.py b/examples/python/sudoku_sat.py index 74134afcb9..af8ff218cb 100644 --- a/examples/python/sudoku_sat.py +++ b/examples/python/sudoku_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/python/tasks_and_workers_assignment_sat.py b/examples/python/tasks_and_workers_assignment_sat.py index 54940e377a..f05a9d20c3 100644 --- a/examples/python/tasks_and_workers_assignment_sat.py +++ b/examples/python/tasks_and_workers_assignment_sat.py @@ -98,7 +98,7 @@ def tasks_and_workers_assignment_sat(): solver = cp_model.CpSolver() solver.parameters.max_time_in_seconds = 60 * 60 * 2 objective_printer = ObjectivePrinter() - status = solver.SolveWithSolutionCallback(model, objective_printer) + status = solver.Solve(model, objective_printer) print(solver.ResponseStats()) if status == cp_model.OPTIMAL: diff --git a/examples/python/vendor_scheduling_sat.py b/examples/python/vendor_scheduling_sat.py index 71ab45e761..0d46a0e540 100644 --- a/examples/python/vendor_scheduling_sat.py +++ b/examples/python/vendor_scheduling_sat.py @@ -123,10 +123,11 @@ def main(): # Solve model. solver = cp_model.CpSolver() + solver.parameters.enumerate_all_solutions = True solution_printer = SolutionPrinter(num_vendors, num_hours, possible_schedules, selected_schedules, hours_stat, min_vendors) - status = solver.SearchForAllSolutions(model, solution_printer) + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Statistics') diff --git a/examples/python/wedding_optimal_chart_sat.py b/examples/python/wedding_optimal_chart_sat.py index b8366f6693..21fa0662a1 100644 --- a/examples/python/wedding_optimal_chart_sat.py +++ b/examples/python/wedding_optimal_chart_sat.py @@ -202,7 +202,7 @@ def solve_with_discrete_model(): ### Solve model. solver = cp_model.CpSolver() solution_printer = WeddingChartPrinter(seats, names, num_tables, num_guests) - solver.SolveWithSolutionCallback(model, solution_printer) + solver.Solve(model, solution_printer) print("Statistics") print(" - conflicts : %i" % solver.NumConflicts()) diff --git a/examples/python/zebra_sat.py b/examples/python/zebra_sat.py index 7cc8629708..3ff6039792 100644 --- a/examples/python/zebra_sat.py +++ b/examples/python/zebra_sat.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 # Copyright 2010-2021 Google LLC # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. diff --git a/examples/tests/cp_model_test.py b/examples/tests/cp_model_test.py index d64adb7ebc..914d51e602 100644 --- a/examples/tests/cp_model_test.py +++ b/examples/tests/cp_model_test.py @@ -573,7 +573,8 @@ class CpModelTest(unittest.TestCase): solver = cp_model.CpSolver() solution_counter = SolutionCounter() - status = solver.SearchForAllSolutions(model, solution_counter) + solver.parameters.enumerate_all_solutions = True + status = solver.Solve(model, solution_counter) self.assertEqual(status, cp_model.OPTIMAL) self.assertEqual(4, solution_counter.solution_count()) diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 3852e06499..5b0531504f 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -218,6 +218,11 @@ message CircuitConstraintProto { // - Self-arcs are allowed except for node 0. // - There is no cycle in this graph, except through node 0. // +// Note: Currently this constraint expect all the nodes in [0, num_nodes) to +// have at least one incident arc. The model will be considered invalid if it +// is not the case. You can add self-arc fixed to one to ignore some nodes if +// needed. +// // TODO(user): It is probably possible to generalize this constraint to a // no-cycle in a general graph, or a no-cycle with sum incoming <= 1 and sum // outgoing <= 1 (more efficient implementation). On the other hand, having this diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index b9ba28547d..4d7de872a6 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -277,6 +277,21 @@ std::string ValidateCircuitConstraint(const CpModelProto& model, std::string ValidateRoutesConstraint(const CpModelProto& model, const ConstraintProto& ct) { + int num_nodes = 0; + absl::flat_hash_set nodes; + for (const int node : ct.routes().tails()) { + nodes.insert(node); + num_nodes = std::max(num_nodes, node + 1); + } + for (const int node : ct.routes().heads()) { + nodes.insert(node); + num_nodes = std::max(num_nodes, node + 1); + } + if (num_nodes != nodes.size()) { + return absl::StrCat( + "All nodes in a route constraint must have incident arcs"); + } + const int size = ct.routes().tails().size(); if (ct.routes().heads().size() != size || ct.routes().literals().size() != size) { @@ -1033,7 +1048,6 @@ class ConstraintChecker { const int64_t min_level = ct.reservoir().min_level(); const int64_t max_level = ct.reservoir().max_level(); std::map deltas; - deltas[0] = 0; const bool has_active_variables = ct.reservoir().actives_size() > 0; for (int i = 0; i < num_variables; i++) { const int64_t time = Value(ct.reservoir().times(i)); diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index d7b57c1881..cea1d7e9aa 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -14,6 +14,7 @@ #include "ortools/sat/cp_model_search.h" #include +#include #include #include "absl/container/flat_hash_map.h" @@ -115,7 +116,7 @@ const std::function ConstructSearchStrategyInternal( return [&view, ¶meters, random, strategies]() { for (const DecisionStrategyProto& strategy : strategies) { int candidate; - int64_t candidate_value = kint64max; + int64_t candidate_value = std::numeric_limits::max(); // TODO(user): Improve the complexity if this becomes an issue which // may be the case if we do a fixed_search. @@ -187,7 +188,7 @@ const std::function ConstructSearchStrategyInternal( } } - if (candidate_value == kint64max) continue; + if (candidate_value == std::numeric_limits::max()) continue; if (parameters.randomize_search()) { CHECK(!active_refs.empty()); const IntegerValue threshold( diff --git a/ortools/sat/cp_model_search.h b/ortools/sat/cp_model_search.h index 7100601323..bdc251a47f 100644 --- a/ortools/sat/cp_model_search.h +++ b/ortools/sat/cp_model_search.h @@ -14,6 +14,7 @@ #ifndef OR_TOOLS_SAT_CP_MODEL_SEARCH_H_ #define OR_TOOLS_SAT_CP_MODEL_SEARCH_H_ +#include #include #include diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 155002d273..7ee29be62d 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -564,12 +564,13 @@ void TryToAddCutGenerators(const CpModelProto& model_proto, const IntegerVariable capacity = mapping->Integer(ct.cumulative().capacity()); relaxation->cut_generators.push_back( - CreateOverlappingCumulativeCutGenerator(intervals, capacity, demands, + CreateCumulativeOverlappingCutGenerator(intervals, capacity, demands, m)); relaxation->cut_generators.push_back( CreateCumulativeCutGenerator(intervals, capacity, demands, m)); relaxation->cut_generators.push_back( - CreateBalasAreaCumulativeCutGenerator(intervals, capacity, demands, m)); + CreateCumulativeCompletionTimeCutGenerator(intervals, capacity, demands, + m)); } if (ct.constraint_case() == ConstraintProto::ConstraintCase::kNoOverlap) { @@ -582,7 +583,7 @@ void TryToAddCutGenerators(const CpModelProto& model_proto, relaxation->cut_generators.push_back( CreateNoOverlapPrecedenceCutGenerator(intervals, m)); relaxation->cut_generators.push_back( - CreateNoOverlapBalasCutGenerator(intervals, m)); + CreateNoOverlapCompletionTimeCutGenerator(intervals, m)); } if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinMax) { @@ -3053,7 +3054,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { { const std::string error = ValidateCpModel(model_proto); if (!error.empty()) { - SOLVER_LOG(logger, error); + SOLVER_LOG(logger, "Invalid model: ", error); shared_response_manager->MutableResponse()->set_status( CpSolverStatus::MODEL_INVALID); return shared_response_manager->GetResponse(); diff --git a/ortools/sat/csharp/CpSolver.cs b/ortools/sat/csharp/CpSolver.cs index 2602c3e011..0a8ada1267 100644 --- a/ortools/sat/csharp/CpSolver.cs +++ b/ortools/sat/csharp/CpSolver.cs @@ -19,13 +19,7 @@ namespace Google.OrTools.Sat { public class CpSolver { - public CpSolverStatus Solve(CpModel model) - { - SolveWithSolutionCallback(model, null); - return response_.Status; - } - - public CpSolverStatus SolveWithSolutionCallback(CpModel model, SolutionCallback cb) + public CpSolverStatus Solve(CpModel model, SolutionCallback cb = null) { // Setup search. CreateSolveWrapper(); @@ -54,11 +48,17 @@ namespace Google.OrTools.Sat return response_.Status; } + [ObsoleteAttribute("This method is obsolete. Call Solve instead.", false)] + public CpSolverStatus SolveWithSolutionCallback(CpModel model, SolutionCallback cb) + { + return Solve(model, cb); + } + public CpSolverStatus SearchAllSolutions(CpModel model, SolutionCallback cb) { string old_parameters = string_parameters_; string_parameters_ += " enumerate_all_solutions:true"; - SolveWithSolutionCallback(model, cb); + Solve(model, cb); string_parameters_ = old_parameters; return response_.Status; } diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index a6c178f0c9..0b91b16116 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -434,7 +434,8 @@ def BooleanProductSampleSat(): # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = cp_model.VarArraySolutionPrinter([x, y, p]) - solver.SearchForAllSolutions(model, solution_printer) + solver.parameters.enumerate_all_solutions = True + solver.Solve(model, solution_printer) BooleanProductSampleSat() diff --git a/ortools/sat/doc/channeling.md b/ortools/sat/doc/channeling.md index 07cdce4e50..36351dcec7 100644 --- a/ortools/sat/doc/channeling.md +++ b/ortools/sat/doc/channeling.md @@ -101,10 +101,12 @@ def ChannelingSampleSat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, y, b]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) ChannelingSampleSat() @@ -218,9 +220,11 @@ public class ChannelingSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions( + solver.solve( model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { @@ -302,10 +306,11 @@ public class ChannelingSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tell the solver to search for all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, b }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } ``` diff --git a/ortools/sat/doc/integer_arithmetic.md b/ortools/sat/doc/integer_arithmetic.md index c4d3207ead..366c50d53e 100644 --- a/ortools/sat/doc/integer_arithmetic.md +++ b/ortools/sat/doc/integer_arithmetic.md @@ -391,10 +391,12 @@ def earliness_tardiness_cost_sample_sat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, expr]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) earliness_tardiness_cost_sample_sat() @@ -543,9 +545,11 @@ public class EarlinessTardinessCostSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions( + solver.solve( model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { @@ -642,10 +646,11 @@ public class EarlinessTardinessCostSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tell the solver to search for all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } ``` @@ -754,10 +759,12 @@ def step_function_sample_sat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, expr]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) step_function_sample_sat() @@ -909,9 +916,11 @@ public class StepFunctionSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions( + solver.solve( model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { @@ -1012,10 +1021,11 @@ public class StepFunctionSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tells the solver to enumerate all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } ``` diff --git a/ortools/sat/doc/model.md b/ortools/sat/doc/model.md index 8e798de2b1..8e00bfca5f 100644 --- a/ortools/sat/doc/model.md +++ b/ortools/sat/doc/model.md @@ -115,7 +115,7 @@ def SolutionHintingSampleSat(): # Creates a solver and solves. solver = cp_model.CpSolver() solution_printer = cp_model.VarArrayAndObjectiveSolutionPrinter([x, y, z]) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Number of solutions found: %i' % solution_printer.solution_count()) @@ -214,7 +214,7 @@ public class SolutionHintingSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); - solver.solveWithSolutionCallback(model, cb); + solver.solve(model, cb); } static class VarArraySolutionPrinterWithObjective extends CpSolverSolutionCallback { @@ -298,7 +298,7 @@ public class SolutionHintingSampleSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); - CpSolverStatus status = solver.SolveWithSolutionCallback(model, cb); + CpSolverStatus status = solver.Solve(model, cb); } } ``` diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index 08f19ba46d..6c2dfb00cb 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -1298,10 +1298,12 @@ def SchedulingWithCalendarSampleSat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print all solutions. solution_printer = VarArraySolutionPrinter([start, duration, across]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) SchedulingWithCalendarSampleSat() diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index 9c321a6d5e..ce202fe7e4 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -258,7 +258,7 @@ def SolveAndPrintIntermediateSolutionsSampleSat(): # Creates a solver and solves. solver = cp_model.CpSolver() solution_printer = VarArrayAndObjectiveSolutionPrinter([x, y, z]) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Number of solutions found: %i' % solution_printer.solution_count()) @@ -373,7 +373,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); - solver.solveWithSolutionCallback(model, cb); + solver.solve(model, cb); System.out.println(cb.getSolutionCount() + " solutions found."); } @@ -436,7 +436,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z }); - solver.SolveWithSolutionCallback(model, cb); + solver.Solve(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } @@ -451,11 +451,20 @@ register a callback on the solver that will be called at each solution. Please note that it does not work in parallel (i. e. parameter `num_search_workers` > 1). +It also does not work if the model contains an objective. + +The method will return the following: + + * *FEASIBLE* if some solutions have been found + * *INFEASIBLE* if the solver has proved there are no solution + * *OPTIMAL* if all solutions have been found + The exact implementation depends on the target language. ### Python code -To search for all solutions, use the SearchForAllSolutions method. +To search for all solutions, use the Solve() method after setting the correct +parameter. ```python """Code sample that solves a model and displays all solutions.""" @@ -498,7 +507,10 @@ def SearchForAllSolutionsSampleSat(): # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinter([x, y, z]) - status = solver.SearchForAllSolutions(model, solution_printer) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve. + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Number of solutions found: %i' % solution_printer.solution_count()) @@ -561,6 +573,9 @@ int main() { ### Java code +As in Python, CpSolver.solve() must be called after setting the correct +parameter. + ```java package com.google.ortools.sat.samples; @@ -612,7 +627,10 @@ public class SearchForAllSolutionsSampleSat { // Create a solver and solve the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}); - solver.searchAllSolutions(model, cb); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); + // And solve. + solver.solve(model, cb); System.out.println(cb.getSolutionCount() + " solutions found."); } @@ -621,7 +639,8 @@ public class SearchForAllSolutionsSampleSat { ### C\# code -As in Python, CpSolver.SearchAllSolutions() must be called. +As in Python, CpSolver.Solve() must be called after setting the correct string +parameter. ```cs using System; @@ -675,7 +694,10 @@ public class SearchForAllSolutionsSampleSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); - solver.SearchAllSolutions(model, cb); + // Search for all solutions. + solver.StringParameters = "enumerate_all_solutions:true"; + // And solve. + solver.Solve(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } @@ -734,7 +756,10 @@ def StopAfterNSolutionsSampleSat(): # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinterWithLimit([x, y, z], 5) - status = solver.SearchForAllSolutions(model, solution_printer) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve. + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Number of solutions found: %i' % solution_printer.solution_count()) assert solution_printer.solution_count() == 5 @@ -866,7 +891,10 @@ public class StopAfterNSolutionsSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5); - solver.searchAllSolutions(model, cb); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); + // And solve. + solver.solve(model, cb); System.out.println(cb.getSolutionCount() + " solutions found."); if (cb.getSolutionCount() != 5) { @@ -935,7 +963,8 @@ public class StopAfterNSolutionsSampleSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); - solver.SearchAllSolutions(model, cb); + solver.StringParameters = "enumerate_all_solutions:true"; + solver.Solve(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } } diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index d96bea46e5..1d294a4ae6 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -1417,8 +1417,8 @@ bool LinearProgrammingConstraint::Propagate() { // problems there is no other constriants than the cuts. cuts_round++; if (num_solves_ > 1) { - implied_bounds_processor_.ClearCache(); - implied_bounds_processor_.SeparateSomeImpliedBoundCuts( + // This must be called first. + implied_bounds_processor_.RecomputeCacheAndSeparateSomeImpliedBoundCuts( expanded_lp_solution_); // The "generic" cuts are currently part of this class as they are using diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 39ae9af434..9f6ed73635 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -1828,7 +1828,9 @@ class CpSolver(object): return self.Solve(model, callback) def SearchForAllSolutions(self, model, callback): - """Search for all solutions of a satisfiability problem. + """DEPRECATED Use Solve() with the right parameter. + + Search for all solutions of a satisfiability problem. This method searches for all feasible solutions of a given model. Then it feeds the solution to the callback. diff --git a/ortools/sat/samples/ChannelingSampleSat.cs b/ortools/sat/samples/ChannelingSampleSat.cs index a7b184bc98..60839fee66 100644 --- a/ortools/sat/samples/ChannelingSampleSat.cs +++ b/ortools/sat/samples/ChannelingSampleSat.cs @@ -68,9 +68,10 @@ public class ChannelingSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tell the solver to search for all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, b }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } diff --git a/ortools/sat/samples/ChannelingSampleSat.java b/ortools/sat/samples/ChannelingSampleSat.java index 8ce5acb9a3..5792ac2982 100644 --- a/ortools/sat/samples/ChannelingSampleSat.java +++ b/ortools/sat/samples/ChannelingSampleSat.java @@ -56,9 +56,11 @@ public class ChannelingSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions(model, new CpSolverSolutionCallback() { + solver.solve(model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { variableArray = variables; return this; diff --git a/ortools/sat/samples/CpIsFunSat.cs b/ortools/sat/samples/CpIsFunSat.cs index 2960b3bcf7..0a9cbb9e4f 100644 --- a/ortools/sat/samples/CpIsFunSat.cs +++ b/ortools/sat/samples/CpIsFunSat.cs @@ -84,7 +84,10 @@ public class CpIsFunSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(letters); - solver.SearchAllSolutions(model, cb); + // Search for all solutions. + solver.StringParameters = "enumerate_all_solutions:true"; + // And solve. + solver.Solve(model, cb); // [END solve] Console.WriteLine("Statistics"); diff --git a/ortools/sat/samples/CpIsFunSat.java b/ortools/sat/samples/CpIsFunSat.java index 57fdfd577c..cdc90f8ed6 100644 --- a/ortools/sat/samples/CpIsFunSat.java +++ b/ortools/sat/samples/CpIsFunSat.java @@ -84,7 +84,10 @@ public class CpIsFunSat { // Create a solver and solve the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(letters); - solver.searchAllSolutions(model, cb); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); + // And solve. + solver.solve(model, cb); // [END solve] System.out.println("Statistics"); diff --git a/ortools/sat/samples/EarlinessTardinessCostSampleSat.cs b/ortools/sat/samples/EarlinessTardinessCostSampleSat.cs index c554286250..4e9798287c 100644 --- a/ortools/sat/samples/EarlinessTardinessCostSampleSat.cs +++ b/ortools/sat/samples/EarlinessTardinessCostSampleSat.cs @@ -83,9 +83,10 @@ public class EarlinessTardinessCostSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tell the solver to search for all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } diff --git a/ortools/sat/samples/EarlinessTardinessCostSampleSat.java b/ortools/sat/samples/EarlinessTardinessCostSampleSat.java index 4083107ef5..4b84e34690 100644 --- a/ortools/sat/samples/EarlinessTardinessCostSampleSat.java +++ b/ortools/sat/samples/EarlinessTardinessCostSampleSat.java @@ -72,9 +72,11 @@ public class EarlinessTardinessCostSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions(model, new CpSolverSolutionCallback() { + solver.solve(model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { variableArray = variables; return this; diff --git a/ortools/sat/samples/SearchForAllSolutionsSampleSat.cs b/ortools/sat/samples/SearchForAllSolutionsSampleSat.cs index 9ead81a588..068f3dde59 100644 --- a/ortools/sat/samples/SearchForAllSolutionsSampleSat.cs +++ b/ortools/sat/samples/SearchForAllSolutionsSampleSat.cs @@ -72,7 +72,10 @@ public class SearchForAllSolutionsSampleSat // [START solve] CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); - solver.SearchAllSolutions(model, cb); + // Search for all solutions. + solver.StringParameters = "enumerate_all_solutions:true"; + // And solve. + solver.Solve(model, cb); // [END solve] Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); diff --git a/ortools/sat/samples/SearchForAllSolutionsSampleSat.java b/ortools/sat/samples/SearchForAllSolutionsSampleSat.java index 5cea26ebd0..1193e52094 100644 --- a/ortools/sat/samples/SearchForAllSolutionsSampleSat.java +++ b/ortools/sat/samples/SearchForAllSolutionsSampleSat.java @@ -71,7 +71,10 @@ public class SearchForAllSolutionsSampleSat { // [START solve] CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}); - solver.searchAllSolutions(model, cb); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); + // And solve. + solver.solve(model, cb); // [END solve] System.out.println(cb.getSolutionCount() + " solutions found."); diff --git a/ortools/sat/samples/SolutionHintingSampleSat.cs b/ortools/sat/samples/SolutionHintingSampleSat.cs index ec2e43f586..8e04187700 100644 --- a/ortools/sat/samples/SolutionHintingSampleSat.cs +++ b/ortools/sat/samples/SolutionHintingSampleSat.cs @@ -80,7 +80,7 @@ public class SolutionHintingSampleSat // [START solve] CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); - CpSolverStatus status = solver.SolveWithSolutionCallback(model, cb); + CpSolverStatus status = solver.Solve(model, cb); // [END solve] } } diff --git a/ortools/sat/samples/SolutionHintingSampleSat.java b/ortools/sat/samples/SolutionHintingSampleSat.java index c47544bb27..b559fc6b6a 100644 --- a/ortools/sat/samples/SolutionHintingSampleSat.java +++ b/ortools/sat/samples/SolutionHintingSampleSat.java @@ -57,7 +57,7 @@ public class SolutionHintingSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); - solver.solveWithSolutionCallback(model, cb); + solver.solve(model, cb); // [END solve] } diff --git a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.cs b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.cs index 03fb80d998..80ef7d5ae5 100644 --- a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.cs +++ b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.cs @@ -76,7 +76,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat // [START solve] CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z }); - solver.SolveWithSolutionCallback(model, cb); + solver.Solve(model, cb); // [END solve] Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); diff --git a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java index f9a99e3853..7a25926c2b 100644 --- a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java +++ b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java @@ -79,7 +79,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); - solver.solveWithSolutionCallback(model, cb); + solver.solve(model, cb); // [END solve] System.out.println(cb.getSolutionCount() + " solutions found."); diff --git a/ortools/sat/samples/StepFunctionSampleSat.cs b/ortools/sat/samples/StepFunctionSampleSat.cs index a5730c4bcb..6a25f51210 100644 --- a/ortools/sat/samples/StepFunctionSampleSat.cs +++ b/ortools/sat/samples/StepFunctionSampleSat.cs @@ -87,9 +87,10 @@ public class StepFunctionSampleSat CpSolver solver = new CpSolver(); // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Tells the solver to enumerate all solutions. + solver.StringParameters = "search_branching:FIXED_SEARCH, enumerate_all_solutions:true"; VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); - solver.SearchAllSolutions(model, cb); + solver.Solve(model, cb); } } diff --git a/ortools/sat/samples/StepFunctionSampleSat.java b/ortools/sat/samples/StepFunctionSampleSat.java index b821077c0d..0a3aa2cd45 100644 --- a/ortools/sat/samples/StepFunctionSampleSat.java +++ b/ortools/sat/samples/StepFunctionSampleSat.java @@ -76,9 +76,11 @@ public class StepFunctionSampleSat { // Force the solver to follow the decision strategy exactly. solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); // Solve the problem with the printer callback. - solver.searchAllSolutions(model, new CpSolverSolutionCallback() { + solver.solve(model, new CpSolverSolutionCallback() { public CpSolverSolutionCallback init(IntVar[] variables) { variableArray = variables; return this; diff --git a/ortools/sat/samples/StopAfterNSolutionsSampleSat.cs b/ortools/sat/samples/StopAfterNSolutionsSampleSat.cs index e68477213b..7fbf8ec3da 100644 --- a/ortools/sat/samples/StopAfterNSolutionsSampleSat.cs +++ b/ortools/sat/samples/StopAfterNSolutionsSampleSat.cs @@ -63,7 +63,8 @@ public class StopAfterNSolutionsSampleSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); - solver.SearchAllSolutions(model, cb); + solver.StringParameters = "enumerate_all_solutions:true"; + solver.Solve(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } } diff --git a/ortools/sat/samples/StopAfterNSolutionsSampleSat.java b/ortools/sat/samples/StopAfterNSolutionsSampleSat.java index b4c2d7822d..18c4b6dcb3 100644 --- a/ortools/sat/samples/StopAfterNSolutionsSampleSat.java +++ b/ortools/sat/samples/StopAfterNSolutionsSampleSat.java @@ -64,7 +64,10 @@ public class StopAfterNSolutionsSampleSat { CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5); - solver.searchAllSolutions(model, cb); + // Tell the solver to enumerate all solutions. + solver.getParameters().setEnumerateAllSolutions(true); + // And solve. + solver.solve(model, cb); System.out.println(cb.getSolutionCount() + " solutions found."); if (cb.getSolutionCount() != 5) { diff --git a/ortools/sat/samples/boolean_product_sample_sat.py b/ortools/sat/samples/boolean_product_sample_sat.py index 9d1d6e4dc1..13bb3f96b5 100644 --- a/ortools/sat/samples/boolean_product_sample_sat.py +++ b/ortools/sat/samples/boolean_product_sample_sat.py @@ -36,7 +36,8 @@ def BooleanProductSampleSat(): # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = cp_model.VarArraySolutionPrinter([x, y, p]) - solver.SearchForAllSolutions(model, solution_printer) + solver.parameters.enumerate_all_solutions = True + solver.Solve(model, solution_printer) BooleanProductSampleSat() diff --git a/ortools/sat/samples/channeling_sample_sat.py b/ortools/sat/samples/channeling_sample_sat.py index 4d7a6960c8..9a199a36d3 100644 --- a/ortools/sat/samples/channeling_sample_sat.py +++ b/ortools/sat/samples/channeling_sample_sat.py @@ -66,10 +66,12 @@ def ChannelingSampleSat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, y, b]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) ChannelingSampleSat() diff --git a/ortools/sat/samples/cp_is_fun_sat.py b/ortools/sat/samples/cp_is_fun_sat.py index e381e79c1e..883aa643b5 100644 --- a/ortools/sat/samples/cp_is_fun_sat.py +++ b/ortools/sat/samples/cp_is_fun_sat.py @@ -84,7 +84,10 @@ def CPIsFunSat(): ### Solve model. solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinter(letters) - status = solver.SearchForAllSolutions(model, solution_printer) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve. + status = solver.Solve(model, solution_printer) # [END solve] print() diff --git a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py index 48a694d0ec..86f85f538c 100644 --- a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py +++ b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py @@ -80,10 +80,12 @@ def earliness_tardiness_cost_sample_sat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, expr]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) earliness_tardiness_cost_sample_sat() diff --git a/ortools/sat/samples/nurses_sat.py b/ortools/sat/samples/nurses_sat.py index 47562cb6e6..bc4aac9b8c 100644 --- a/ortools/sat/samples/nurses_sat.py +++ b/ortools/sat/samples/nurses_sat.py @@ -117,12 +117,14 @@ def main(): # [START solve] solver = cp_model.CpSolver() solver.parameters.linearization_level = 0 + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Display the first five solutions. a_few_solutions = range(5) solution_printer = NursesPartialSolutionPrinter(shifts, num_nurses, num_days, num_shifts, a_few_solutions) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) # [END solve] # Statistics. diff --git a/ortools/sat/samples/scheduling_with_calendar_sample_sat.py b/ortools/sat/samples/scheduling_with_calendar_sample_sat.py index c5436f2193..4d09a5aab1 100644 --- a/ortools/sat/samples/scheduling_with_calendar_sample_sat.py +++ b/ortools/sat/samples/scheduling_with_calendar_sample_sat.py @@ -70,10 +70,12 @@ def SchedulingWithCalendarSampleSat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print all solutions. solution_printer = VarArraySolutionPrinter([start, duration, across]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) SchedulingWithCalendarSampleSat() diff --git a/ortools/sat/samples/search_for_all_solutions_sample_sat.py b/ortools/sat/samples/search_for_all_solutions_sample_sat.py index eb9c9d57de..455b8db674 100644 --- a/ortools/sat/samples/search_for_all_solutions_sample_sat.py +++ b/ortools/sat/samples/search_for_all_solutions_sample_sat.py @@ -61,7 +61,10 @@ def SearchForAllSolutionsSampleSat(): # [START solve] solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinter([x, y, z]) - status = solver.SearchForAllSolutions(model, solution_printer) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve. + status = solver.Solve(model, solution_printer) # [END solve] print('Status = %s' % solver.StatusName(status)) diff --git a/ortools/sat/samples/solution_hinting_sample_sat.py b/ortools/sat/samples/solution_hinting_sample_sat.py index 641b2fa48d..7a4881c9ad 100644 --- a/ortools/sat/samples/solution_hinting_sample_sat.py +++ b/ortools/sat/samples/solution_hinting_sample_sat.py @@ -49,7 +49,7 @@ def SolutionHintingSampleSat(): # [START solve] solver = cp_model.CpSolver() solution_printer = cp_model.VarArrayAndObjectiveSolutionPrinter([x, y, z]) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) # [END solve] print('Status = %s' % solver.StatusName(status)) diff --git a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py index e205128cde..daa9fc38f8 100644 --- a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py +++ b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py @@ -68,7 +68,7 @@ def SolveAndPrintIntermediateSolutionsSampleSat(): # [START solve] solver = cp_model.CpSolver() solution_printer = VarArrayAndObjectiveSolutionPrinter([x, y, z]) - status = solver.SolveWithSolutionCallback(model, solution_printer) + status = solver.Solve(model, solution_printer) # [END solve] print('Status = %s' % solver.StatusName(status)) diff --git a/ortools/sat/samples/step_function_sample_sat.py b/ortools/sat/samples/step_function_sample_sat.py index eb6549e732..da7c38e9f4 100644 --- a/ortools/sat/samples/step_function_sample_sat.py +++ b/ortools/sat/samples/step_function_sample_sat.py @@ -84,10 +84,12 @@ def step_function_sample_sat(): # Force the solver to follow the decision strategy exactly. solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True # Search and print out all solutions. solution_printer = VarArraySolutionPrinter([x, expr]) - solver.SearchForAllSolutions(model, solution_printer) + solver.Solve(model, solution_printer) step_function_sample_sat() diff --git a/ortools/sat/samples/stop_after_n_solutions_sample_sat.py b/ortools/sat/samples/stop_after_n_solutions_sample_sat.py index 6f74848d06..67f2841774 100644 --- a/ortools/sat/samples/stop_after_n_solutions_sample_sat.py +++ b/ortools/sat/samples/stop_after_n_solutions_sample_sat.py @@ -51,7 +51,10 @@ def StopAfterNSolutionsSampleSat(): # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinterWithLimit([x, y, z], 5) - status = solver.SearchForAllSolutions(model, solution_printer) + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + # Solve. + status = solver.Solve(model, solution_printer) print('Status = %s' % solver.StatusName(status)) print('Number of solutions found: %i' % solution_printer.solution_count()) assert solution_printer.solution_count() == 5