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

[CP-SAT] convert to PEP8 convention

Browse Source
This commit is contained in:
Laurent Perron
2023-11-16 19:46:56 +01:00
parent 7f48cd9a9a
commit 5b6c803db3
103 changed files with 4648 additions and 3430 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
examples/python/appointments.py Executable file → Normal file
View File

@@ -44,17 +44,19 @@ class AllSolutionCollector(cp_model.CpSolverSolutionCallback):
self.__variables = variables
self.__collect = []
def on_solution_callback(self):
def on_solution_callback(self) -> None:
"""Collect a new combination."""
combination = [self.Value(v) for v in self.__variables]
combination = [self.value(v) for v in self.__variables]
self.__collect.append(combination)
def combinations(self):
def combinations(self) -> list[list[int]]:
"""Returns all collected combinations."""
return self.__collect
def EnumerateAllKnapsacksWithRepetition(item_sizes, total_size_min, total_size_max):
def EnumerateAllKnapsacksWithRepetition(
item_sizes: list[int], total_size_min: int, total_size_max: int
) -> list[list[int]]:
"""Enumerate all possible knapsacks with total size in the given range.
Args:
@@ -68,22 +70,26 @@ def EnumerateAllKnapsacksWithRepetition(item_sizes, total_size_min, total_size_m
nonnegative integer: the number of times we put item #K in the knapsack.
"""
model = cp_model.CpModel()
variables = [model.NewIntVar(0, total_size_max // size, "") for size in item_sizes]
variables = [
model.new_int_var(0, total_size_max // size, "") for size in item_sizes
]
load = sum(variables[i] * size for i, size in enumerate(item_sizes))
model.AddLinearConstraint(load, total_size_min, total_size_max)
model.add_linear_constraint(load, total_size_min, total_size_max)
solver = cp_model.CpSolver()
solution_collector = AllSolutionCollector(variables)
# Enumerate all solutions.
solver.parameters.enumerate_all_solutions = True
# Solve
solver.Solve(model, solution_collector)
# solve
solver.solve(model, solution_collector)
return solution_collector.combinations()
def AggregateItemCollectionsOptimally(
item_collections, max_num_collections, ideal_item_ratios
):
item_collections: list[list[int]],
max_num_collections: int,
ideal_item_ratios: list[float],
) -> list[int]:
"""Selects a set (with repetition) of combination of items optimally.
Given a set of collections of N possible items (in each collection, an item
@@ -173,7 +179,9 @@ def AggregateItemCollectionsOptimally(
return []
def GetOptimalSchedule(demand):
def GetOptimalSchedule(
demand: list[tuple[float, str, int]]
) -> list[tuple[int, list[tuple[int, str]]]]:
"""Computes the optimal schedule for the installation input.
Args:
@@ -186,7 +194,9 @@ def GetOptimalSchedule(demand):
The same output type as EnumerateAllKnapsacksWithRepetition.
"""
combinations = EnumerateAllKnapsacksWithRepetition(
[a[2] + _COMMUTE_TIME.value for a in demand], _LOAD_MIN.value, _LOAD_MAX.value
[a[2] + _COMMUTE_TIME.value for a in demand],
_LOAD_MIN.value,
_LOAD_MAX.value,
)
print(
(
@@ -199,14 +209,14 @@ def GetOptimalSchedule(demand):
combinations, _NUM_WORKERS.value, [a[0] / 100.0 for a in demand]
)
output = []
for i in range(len(selection)):
if selection[i] != 0:
for i, s in enumerate(selection):
if s != 0:
output.append(
(
selection[i],
s,
[
(combinations[i][t], demand[t][1])
for t in range(len(demand))
(combinations[i][t], d[1])
for t, d in enumerate(demand)
if combinations[i][t] != 0
],
)
@@ -252,7 +262,8 @@ def main(_):
per_type = installed_per_type[name]
if installed != 0:
print(
f" {per_type} ({per_type * 100.0 / installed}%) installations of type {name} planned"
f" {per_type} ({per_type * 100.0 / installed}%) installations of"
f" type {name} planned"
)
else:
print(f" {per_type} installations of type {name} planned")

35
examples/python/assignment_with_constraints_sat.py
View File

@@ -12,7 +12,7 @@
# See the License for the specific language governing permissions and
# limitations under the License.
"""Solve an assignment problem with combination constraints on workers."""
"""solve an assignment problem with combination constraints on workers."""
from typing import Sequence
from absl import app
@@ -20,7 +20,7 @@ from ortools.sat.python import cp_model
def solve_assignment():
"""Solve the assignment problem."""
"""solve the assignment problem."""
# Data.
cost = [
[90, 76, 75, 70, 50, 74],
@@ -73,44 +73,45 @@ def solve_assignment():
model = cp_model.CpModel()
# Variables
selected = [
[model.NewBoolVar("x[%i,%i]" % (i, j)) for j in all_tasks] for i in all_workers
[model.new_bool_var("x[%i,%i]" % (i, j)) for j in all_tasks]
for i in all_workers
]
works = [model.NewBoolVar("works[%i]" % i) for i in all_workers]
works = [model.new_bool_var("works[%i]" % i) for i in all_workers]
# Constraints
# Link selected and workers.
for i in range(num_workers):
model.AddMaxEquality(works[i], selected[i])
model.add_max_equality(works[i], selected[i])
# Each task is assigned to at least one worker.
for j in all_tasks:
model.Add(sum(selected[i][j] for i in all_workers) >= 1)
model.add(sum(selected[i][j] for i in all_workers) >= 1)
# Total task size for each worker is at most total_size_max
for i in all_workers:
model.Add(sum(sizes[j] * selected[i][j] for j in all_tasks) <= total_size_max)
model.add(sum(sizes[j] * selected[i][j] for j in all_tasks) <= total_size_max)
# Group constraints.
model.AddAllowedAssignments([works[0], works[1], works[2], works[3]], group1)
model.AddAllowedAssignments([works[4], works[5], works[6], works[7]], group2)
model.AddAllowedAssignments([works[8], works[9], works[10], works[11]], group3)
model.add_allowed_assignments([works[0], works[1], works[2], works[3]], group1)
model.add_allowed_assignments([works[4], works[5], works[6], works[7]], group2)
model.add_allowed_assignments([works[8], works[9], works[10], works[11]], group3)
# Objective
model.Minimize(
model.minimize(
sum(selected[i][j] * cost[i][j] for j in all_tasks for i in all_workers)
)
# Solve and output solution.
solver = cp_model.CpSolver()
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print("Total cost = %i" % solver.ObjectiveValue())
print("Total cost = %i" % solver.objective_value)
print()
for i in all_workers:
for j in all_tasks:
if solver.BooleanValue(selected[i][j]):
if solver.boolean_value(selected[i][j]):
print(
"Worker ", i, " assigned to task ", j, " Cost = ", cost[i][j]
)
@@ -118,9 +119,9 @@ def solve_assignment():
print()
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
def main(argv: Sequence[str]) -> None:

42
examples/python/balance_group_sat.py
View File

@@ -41,14 +41,14 @@ class SolutionPrinter(cp_model.CpSolverSolutionCallback):
print("Solution %i" % self.__solution_count)
self.__solution_count += 1
print(" objective value = %i" % self.ObjectiveValue())
print(" objective value = %i" % self.objective_value)
groups = {}
sums = {}
for g in self.__all_groups:
groups[g] = []
sums[g] = 0
for item in self.__all_items:
if self.BooleanValue(self.__item_in_group[(item, g)]):
if self.boolean_value(self.__item_in_group[(item, g)]):
groups[g].append(item)
sums[g] += self.__values[item]
@@ -77,7 +77,7 @@ def main(argv: Sequence[str]) -> None:
all_items = range(num_items)
all_colors = range(num_colors)
# Values for each items.
# values for each items.
values = [1 + i + (i * i // 200) for i in all_items]
# Color for each item (simple modulo).
colors = [i % num_colors for i in all_items]
@@ -108,26 +108,26 @@ def main(argv: Sequence[str]) -> None:
item_in_group = {}
for i in all_items:
for g in all_groups:
item_in_group[(i, g)] = model.NewBoolVar("item %d in group %d" % (i, g))
item_in_group[(i, g)] = model.new_bool_var("item %d in group %d" % (i, g))
# Each group must have the same size.
for g in all_groups:
model.Add(sum(item_in_group[(i, g)] for i in all_items) == num_items_per_group)
model.add(sum(item_in_group[(i, g)] for i in all_items) == num_items_per_group)
# One item must belong to exactly one group.
for i in all_items:
model.Add(sum(item_in_group[(i, g)] for g in all_groups) == 1)
model.add(sum(item_in_group[(i, g)] for g in all_groups) == 1)
# The deviation of the sum of each items in a group against the average.
e = model.NewIntVar(0, 550, "epsilon")
e = model.new_int_var(0, 550, "epsilon")
# Constrain the sum of values in one group around the average sum per group.
for g in all_groups:
model.Add(
model.add(
sum(item_in_group[(i, g)] * values[i] for i in all_items)
<= average_sum_per_group + e
)
model.Add(
model.add(
sum(item_in_group[(i, g)] * values[i] for i in all_items)
>= average_sum_per_group - e
)
@@ -136,24 +136,24 @@ def main(argv: Sequence[str]) -> None:
color_in_group = {}
for g in all_groups:
for c in all_colors:
color_in_group[(c, g)] = model.NewBoolVar(
color_in_group[(c, g)] = model.new_bool_var(
"color %d is in group %d" % (c, g)
)
# Item is in a group implies its color is in that group.
for i in all_items:
for g in all_groups:
model.AddImplication(item_in_group[(i, g)], color_in_group[(colors[i], g)])
model.add_implication(item_in_group[(i, g)], color_in_group[(colors[i], g)])
# If a color is in a group, it must contains at least
# min_items_of_same_color_per_group items from that color.
for c in all_colors:
for g in all_groups:
literal = color_in_group[(c, g)]
model.Add(
model.add(
sum(item_in_group[(i, g)] for i in items_per_color[c])
>= min_items_of_same_color_per_group
).OnlyEnforceIf(literal)
).only_enforce_if(literal)
# Compute the maximum number of colors in a group.
max_color = num_items_per_group // min_items_of_same_color_per_group
@@ -161,10 +161,10 @@ def main(argv: Sequence[str]) -> None:
# Redundant constraint, it helps with solving time.
if max_color < num_colors:
for g in all_groups:
model.Add(sum(color_in_group[(c, g)] for c in all_colors) <= max_color)
model.add(sum(color_in_group[(c, g)] for c in all_colors) <= max_color)
# Minimize epsilon
model.Minimize(e)
# minimize epsilon
model.minimize(e)
solver = cp_model.CpSolver()
# solver.parameters.log_search_progress = True
@@ -172,14 +172,14 @@ def main(argv: Sequence[str]) -> None:
solution_printer = SolutionPrinter(
values, colors, all_groups, all_items, item_in_group
)
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
if status == cp_model.OPTIMAL:
print("Optimal epsilon: %i" % solver.ObjectiveValue())
print("Optimal epsilon: %i" % solver.objective_value)
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
else:
print("No solution found")

142
examples/python/bus_driver_scheduling_sat.py
View File

@@ -1708,7 +1708,7 @@ SAMPLE_SHIFTS_LARGE = [
] # yapf:disable
def bus_driver_scheduling(minimize_drivers, max_num_drivers):
def bus_driver_scheduling(minimize_drivers: bool, max_num_drivers: int) -> int:
"""Optimize the bus driver scheduling problem.
This model has two modes.
@@ -1806,14 +1806,14 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
for d in range(num_drivers):
start_times.append(
model.NewIntVar(min_start_time - setup_time, max_end_time, "start_%i" % d)
model.new_int_var(min_start_time - setup_time, max_end_time, "start_%i" % d)
)
end_times.append(
model.NewIntVar(min_start_time, max_end_time + cleanup_time, "end_%i" % d)
model.new_int_var(min_start_time, max_end_time + cleanup_time, "end_%i" % d)
)
driving_times.append(model.NewIntVar(0, max_driving_time, "driving_%i" % d))
driving_times.append(model.new_int_var(0, max_driving_time, "driving_%i" % d))
working_times.append(
model.NewIntVar(0, max_working_time, "working_times_%i" % d)
model.new_int_var(0, max_working_time, "working_times_%i" % d)
)
incoming_literals = collections.defaultdict(list)
@@ -1824,13 +1824,13 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
# Create all the shift variables before iterating on the transitions
# between these shifts.
for s in range(num_shifts):
total_driving[d, s] = model.NewIntVar(
total_driving[d, s] = model.new_int_var(
0, max_driving_time, "dr_%i_%i" % (d, s)
)
no_break_driving[d, s] = model.NewIntVar(
no_break_driving[d, s] = model.new_int_var(
0, max_driving_time_without_pauses, "mdr_%i_%i" % (d, s)
)
performed[d, s] = model.NewBoolVar("performed_%i_%i" % (d, s))
performed[d, s] = model.new_bool_var("performed_%i_%i" % (d, s))
for s in range(num_shifts):
shift = shifts[s]
@@ -1839,42 +1839,48 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
# Arc from source to shift.
# - set the start time of the driver
# - increase driving time and driving time since break
source_lit = model.NewBoolVar("%i from source to %i" % (d, s))
source_lit = model.new_bool_var("%i from source to %i" % (d, s))
outgoing_source_literals.append(source_lit)
incoming_literals[s].append(source_lit)
shared_incoming_literals[s].append(source_lit)
model.Add(start_times[d] == shift[3] - setup_time).OnlyEnforceIf(source_lit)
model.Add(total_driving[d, s] == duration).OnlyEnforceIf(source_lit)
model.Add(no_break_driving[d, s] == duration).OnlyEnforceIf(source_lit)
model.add(start_times[d] == shift[3] - setup_time).only_enforce_if(
source_lit
)
model.add(total_driving[d, s] == duration).only_enforce_if(source_lit)
model.add(no_break_driving[d, s] == duration).only_enforce_if(source_lit)
starting_shifts[d, s] = source_lit
# Arc from shift to sink
# - set the end time of the driver
# - set the driving times of the driver
sink_lit = model.NewBoolVar("%i from %i to sink" % (d, s))
sink_lit = model.new_bool_var("%i from %i to sink" % (d, s))
outgoing_literals[s].append(sink_lit)
shared_outgoing_literals[s].append(sink_lit)
incoming_sink_literals.append(sink_lit)
model.Add(end_times[d] == shift[4] + cleanup_time).OnlyEnforceIf(sink_lit)
model.Add(driving_times[d] == total_driving[d, s]).OnlyEnforceIf(sink_lit)
model.add(end_times[d] == shift[4] + cleanup_time).only_enforce_if(sink_lit)
model.add(driving_times[d] == total_driving[d, s]).only_enforce_if(sink_lit)
# Node not performed
# - set both driving times to 0
# - add a looping arc on the node
model.Add(total_driving[d, s] == 0).OnlyEnforceIf(performed[d, s].Not())
model.Add(no_break_driving[d, s] == 0).OnlyEnforceIf(performed[d, s].Not())
incoming_literals[s].append(performed[d, s].Not())
outgoing_literals[s].append(performed[d, s].Not())
# Not adding to the shared lists, because, globally, each node will have
# one incoming literal, and one outgoing literal.
model.add(total_driving[d, s] == 0).only_enforce_if(
performed[d, s].negated()
)
model.add(no_break_driving[d, s] == 0).only_enforce_if(
performed[d, s].negated()
)
incoming_literals[s].append(performed[d, s].negated())
outgoing_literals[s].append(performed[d, s].negated())
# negated adding to the shared lists, because, globally, each node will
# have one incoming literal, and one outgoing literal.
# Node performed:
# - add upper bound on start_time
# - add lower bound on end_times
model.Add(start_times[d] <= shift[3] - setup_time).OnlyEnforceIf(
model.add(start_times[d] <= shift[3] - setup_time).only_enforce_if(
performed[d, s]
)
model.Add(end_times[d] >= shift[4] + cleanup_time).OnlyEnforceIf(
model.add(end_times[d] >= shift[4] + cleanup_time).only_enforce_if(
performed[d, s]
)
@@ -1883,22 +1889,22 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
delay = other[3] - shift[4]
if delay < min_delay_between_shifts:
continue
lit = model.NewBoolVar("%i from %i to %i" % (d, s, o))
lit = model.new_bool_var("%i from %i to %i" % (d, s, o))
# Increase driving time
model.Add(
model.add(
total_driving[d, o] == total_driving[d, s] + other[5]
).OnlyEnforceIf(lit)
).only_enforce_if(lit)
# Increase no_break_driving or reset it to 0 depending on the delay
if delay >= min_pause_after_4h:
model.Add(no_break_driving[d, o] == other[5]).OnlyEnforceIf(lit)
model.add(no_break_driving[d, o] == other[5]).only_enforce_if(lit)
else:
model.Add(
model.add(
no_break_driving[d, o] == no_break_driving[d, s] + other[5]
).OnlyEnforceIf(lit)
).only_enforce_if(lit)
# Add arc
# add arc
outgoing_literals[s].append(lit)
shared_outgoing_literals[s].append(lit)
incoming_literals[o].append(lit)
@@ -1908,68 +1914,72 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
delay_literals.append(lit)
delay_weights.append(delay)
model.Add(working_times[d] == end_times[d] - start_times[d])
model.add(working_times[d] == end_times[d] - start_times[d])
if minimize_drivers:
# Driver is not working.
working = model.NewBoolVar("working_%i" % d)
model.Add(start_times[d] == min_start_time).OnlyEnforceIf(working.Not())
model.Add(end_times[d] == min_start_time).OnlyEnforceIf(working.Not())
model.Add(driving_times[d] == 0).OnlyEnforceIf(working.Not())
working = model.new_bool_var("working_%i" % d)
model.add(start_times[d] == min_start_time).only_enforce_if(
working.negated()
)
model.add(end_times[d] == min_start_time).only_enforce_if(working.negated())
model.add(driving_times[d] == 0).only_enforce_if(working.negated())
working_drivers.append(working)
outgoing_source_literals.append(working.Not())
incoming_sink_literals.append(working.Not())
outgoing_source_literals.append(working.negated())
incoming_sink_literals.append(working.negated())
# Conditional working time constraints
model.Add(working_times[d] >= min_working_time).OnlyEnforceIf(working)
model.Add(working_times[d] == 0).OnlyEnforceIf(working.Not())
model.add(working_times[d] >= min_working_time).only_enforce_if(working)
model.add(working_times[d] == 0).only_enforce_if(working.negated())
else:
# Working time constraints
model.Add(working_times[d] >= min_working_time)
model.add(working_times[d] >= min_working_time)
# Create circuit constraint.
model.AddExactlyOne(outgoing_source_literals)
model.add_exactly_one(outgoing_source_literals)
for s in range(num_shifts):
model.AddExactlyOne(outgoing_literals[s])
model.AddExactlyOne(incoming_literals[s])
model.AddExactlyOne(incoming_sink_literals)
model.add_exactly_one(outgoing_literals[s])
model.add_exactly_one(incoming_literals[s])
model.add_exactly_one(incoming_sink_literals)
# Each shift is covered.
for s in range(num_shifts):
model.AddExactlyOne(performed[d, s] for d in range(num_drivers))
model.add_exactly_one(performed[d, s] for d in range(num_drivers))
# Globally, each node has one incoming and one outgoing literal
model.AddExactlyOne(shared_incoming_literals[s])
model.AddExactlyOne(shared_outgoing_literals[s])
model.add_exactly_one(shared_incoming_literals[s])
model.add_exactly_one(shared_outgoing_literals[s])
# Symmetry breaking
# The first 3 shifts must be performed by 3 different drivers.
# Let's assign them to the first 3 drivers in sequence
model.Add(starting_shifts[0, 0] == 1)
model.Add(starting_shifts[1, 1] == 1)
model.Add(starting_shifts[2, 2] == 1)
model.add(starting_shifts[0, 0] == 1)
model.add(starting_shifts[1, 1] == 1)
model.add(starting_shifts[2, 2] == 1)
if minimize_drivers:
# Push non working drivers to the end
for d in range(num_drivers - 1):
model.AddImplication(working_drivers[d].Not(), working_drivers[d + 1].Not())
model.add_implication(
working_drivers[d].negated(), working_drivers[d + 1].negated()
)
# Redundant constraints: sum of driving times = sum of shift driving times
model.Add(cp_model.LinearExpr.Sum(driving_times) == total_driving_time)
model.add(cp_model.LinearExpr.sum(driving_times) == total_driving_time)
if not minimize_drivers:
model.Add(
cp_model.LinearExpr.Sum(working_times)
model.add(
cp_model.LinearExpr.sum(working_times)
== total_driving_time
+ num_drivers * (setup_time + cleanup_time)
+ cp_model.LinearExpr.WeightedSum(delay_literals, delay_weights)
+ cp_model.LinearExpr.weighted_sum(delay_literals, delay_weights)
)
if minimize_drivers:
# Minimize the number of working drivers
model.Minimize(cp_model.LinearExpr.Sum(working_drivers))
# minimize the number of working drivers
model.minimize(cp_model.LinearExpr.sum(working_drivers))
else:
# Minimize the sum of delays between tasks, which in turns minimize the
# minimize the sum of delays between tasks, which in turns minimize the
# sum of working times as the total driving time is fixed
model.Minimize(cp_model.LinearExpr.WeightedSum(delay_literals, delay_weights))
model.minimize(cp_model.LinearExpr.weighted_sum(delay_literals, delay_weights))
if not minimize_drivers and _OUTPUT_PROTO.value:
print("Writing proto to %s" % _OUTPUT_PROTO.value)
@@ -1981,41 +1991,41 @@ def bus_driver_scheduling(minimize_drivers, max_num_drivers):
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
status = solver.Solve(model)
status = solver.solve(model)
if status != cp_model.OPTIMAL and status != cp_model.FEASIBLE:
return -1
# Display solution
if minimize_drivers:
max_num_drivers = int(solver.ObjectiveValue())
max_num_drivers = int(solver.objective_value)
print("minimal number of drivers =", max_num_drivers)
return max_num_drivers
for d in range(num_drivers):
print("Driver %i: " % (d + 1))
print(" total driving time =", solver.Value(driving_times[d]))
print(" total driving time =", solver.value(driving_times[d]))
print(
" working time =",
solver.Value(working_times[d]) + setup_time + cleanup_time,
solver.value(working_times[d]) + setup_time + cleanup_time,
)
first = True
for s in range(num_shifts):
shift = shifts[s]
if not solver.BooleanValue(performed[d, s]):
if not solver.boolean_value(performed[d, s]):
continue
# Hack to detect if the waiting time between the last shift and
# this one exceeds 30 minutes. For this, we look at the
# no_break_driving which was reinitialized in that case.
if solver.Value(no_break_driving[d, s]) == shift[5] and not first:
if solver.value(no_break_driving[d, s]) == shift[5] and not first:
print(" **break**")
print(" shift ", shift[0], ":", shift[1], "-", shift[2])
first = False
return int(solver.ObjectiveValue())
return int(solver.objective_value)
def main(_):

23
examples/python/chemical_balance_sat.py
View File

@@ -70,37 +70,40 @@ def chemical_balance():
for s in all_sets
]
set_vars = [model.NewIntVar(0, max_set[s], f"set_{s}") for s in all_sets]
set_vars = [model.new_int_var(0, max_set[s], f"set_{s}") for s in all_sets]
epsilon = model.NewIntVar(0, 10000000, "epsilon")
epsilon = model.new_int_var(0, 10000000, "epsilon")
for p in all_products:
model.Add(
model.add(
sum(int(chemical_set[s][p + 1] * 10) * set_vars[s] for s in all_sets)
<= int(max_quantities[p][1] * 10000)
)
model.Add(
model.add(
sum(int(chemical_set[s][p + 1] * 10) * set_vars[s] for s in all_sets)
>= int(max_quantities[p][1] * 10000) - epsilon
)
model.Minimize(epsilon)
model.minimize(epsilon)
# Creates a solver and solves.
solver = cp_model.CpSolver()
status = solver.Solve(model)
print(f"Status = {solver.StatusName(status)}")
status = solver.solve(model)
print(f"Status = {solver.status_name(status)}")
# The objective value of the solution.
print(f"Optimal objective value = {solver.ObjectiveValue() / 10000.0}")
print(f"Optimal objective value = {solver.objective_value / 10000.0}")
for s in all_sets:
print(f" {chemical_set[s][0]} = {solver.Value(set_vars[s]) / 1000.0}", end=" ")
print(
f" {chemical_set[s][0]} = {solver.value(set_vars[s]) / 1000.0}",
end=" ",
)
print()
for p in all_products:
name = max_quantities[p][0]
max_quantity = max_quantities[p][1]
quantity = sum(
solver.Value(set_vars[s]) / 1000.0 * chemical_set[s][p + 1]
solver.value(set_vars[s]) / 1000.0 * chemical_set[s][p + 1]
for s in all_sets
)
print(f"{name}: {quantity} out of {max_quantity}")

16
examples/python/clustering_sat.py
View File

@@ -83,14 +83,14 @@ def clustering_sat():
obj_coeffs = []
for n1 in range(num_nodes - 1):
for n2 in range(n1 + 1, num_nodes):
same = model.NewBoolVar("neighbors_%i_%i" % (n1, n2))
same = model.new_bool_var("neighbors_%i_%i" % (n1, n2))
neighbors[n1, n2] = same
obj_vars.append(same)
obj_coeffs.append(distance_matrix[n1][n2] + distance_matrix[n2][n1])
# Number of neighborss:
for n in range(num_nodes):
model.Add(
model.add(
sum(neighbors[m, n] for m in range(n))
+ sum(neighbors[n, m] for m in range(n + 1, num_nodes))
== group_size - 1
@@ -100,23 +100,23 @@ def clustering_sat():
for n1 in range(num_nodes - 2):
for n2 in range(n1 + 1, num_nodes - 1):
for n3 in range(n2 + 1, num_nodes):
model.Add(
model.add(
neighbors[n1, n3] + neighbors[n2, n3] + neighbors[n1, n2] != 2
)
# Redundant constraints on total sum of neighborss.
model.Add(sum(obj_vars) == num_groups * group_size * (group_size - 1) // 2)
model.add(sum(obj_vars) == num_groups * group_size * (group_size - 1) // 2)
# Minimize weighted sum of arcs.
model.Minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
model.minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
# Solve and print out the solution.
solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
solver.parameters.num_search_workers = 8
status = solver.Solve(model)
print(solver.ResponseStats())
status = solver.solve(model)
print(solver.response_stats())
if status == cp_model.FEASIBLE or status == cp_model.OPTIMAL:
visited = set()
@@ -126,7 +126,7 @@ def clustering_sat():
visited.add(n)
output = str(n)
for o in range(n + 1, num_nodes):
if solver.BooleanValue(neighbors[n, o]):
if solver.boolean_value(neighbors[n, o]):
visited.add(o)
output += " " + str(o)
print("Group", g, ":", output)

55
examples/python/cover_rectangle_sat.py
View File

@@ -19,7 +19,7 @@ from absl import app
from ortools.sat.python import cp_model
def cover_rectangle(num_squares):
def cover_rectangle(num_squares: int) -> bool:
"""Try to fill the rectangle with a given number of squares."""
size_x = 60
size_y = 50
@@ -35,17 +35,17 @@ def cover_rectangle(num_squares):
# Creates intervals for the NoOverlap2D and size variables.
for i in range(num_squares):
size = model.NewIntVar(1, size_y, "size_%i" % i)
start_x = model.NewIntVar(0, size_x, "sx_%i" % i)
end_x = model.NewIntVar(0, size_x, "ex_%i" % i)
start_y = model.NewIntVar(0, size_y, "sy_%i" % i)
end_y = model.NewIntVar(0, size_y, "ey_%i" % i)
size = model.new_int_var(1, size_y, "size_%i" % i)
start_x = model.new_int_var(0, size_x, "sx_%i" % i)
end_x = model.new_int_var(0, size_x, "ex_%i" % i)
start_y = model.new_int_var(0, size_y, "sy_%i" % i)
end_y = model.new_int_var(0, size_y, "ey_%i" % i)
interval_x = model.NewIntervalVar(start_x, size, end_x, "ix_%i" % i)
interval_y = model.NewIntervalVar(start_y, size, end_y, "iy_%i" % i)
interval_x = model.new_interval_var(start_x, size, end_x, "ix_%i" % i)
interval_y = model.new_interval_var(start_y, size, end_y, "iy_%i" % i)
area = model.NewIntVar(1, size_y * size_y, "area_%i" % i)
model.AddMultiplicationEquality(area, [size, size])
area = model.new_int_var(1, size_y * size_y, "area_%i" % i)
model.add_multiplication_equality(area, [size, size])
areas.append(area)
x_intervals.append(interval_x)
@@ -55,47 +55,46 @@ def cover_rectangle(num_squares):
y_starts.append(start_y)
# Main constraint.
model.AddNoOverlap2D(x_intervals, y_intervals)
model.add_no_overlap_2d(x_intervals, y_intervals)
# Redundant constraints.
model.AddCumulative(x_intervals, sizes, size_y)
model.AddCumulative(y_intervals, sizes, size_x)
model.add_cumulative(x_intervals, sizes, size_y)
model.add_cumulative(y_intervals, sizes, size_x)
# Forces the rectangle to be exactly covered.
model.Add(sum(areas) == size_x * size_y)
model.add(sum(areas) == size_x * size_y)
# Symmetry breaking 1: sizes are ordered.
for i in range(num_squares - 1):
model.Add(sizes[i] <= sizes[i + 1])
model.add(sizes[i] <= sizes[i + 1])
# Define same to be true iff sizes[i] == sizes[i + 1]
same = model.NewBoolVar("")
model.Add(sizes[i] == sizes[i + 1]).OnlyEnforceIf(same)
model.Add(sizes[i] < sizes[i + 1]).OnlyEnforceIf(same.Not())
same = model.new_bool_var("")
model.add(sizes[i] == sizes[i + 1]).only_enforce_if(same)
model.add(sizes[i] < sizes[i + 1]).only_enforce_if(same.negated())
# Tie break with starts.
model.Add(x_starts[i] <= x_starts[i + 1]).OnlyEnforceIf(same)
model.add(x_starts[i] <= x_starts[i + 1]).only_enforce_if(same)
# Symmetry breaking 2: first square in one quadrant.
model.Add(x_starts[0] < (size_x + 1) // 2)
model.Add(y_starts[0] < (size_y + 1) // 2)
model.add(x_starts[0] < (size_x + 1) // 2)
model.add(y_starts[0] < (size_y + 1) // 2)
# Creates a solver and solves.
solver = cp_model.CpSolver()
solver.parameters.num_workers = 16
# solver.parameters.log_search_progress = True
solver.parameters.num_workers = 8
solver.parameters.max_time_in_seconds = 10.0
status = solver.Solve(model)
print("%s found in %0.2fs" % (solver.StatusName(status), solver.WallTime()))
status = solver.solve(model)
print("%s found in %0.2fs" % (solver.status_name(status), solver.wall_time))
# Prints solution.
solution_found = status == cp_model.OPTIMAL or status == cp_model.FEASIBLE
if solution_found:
display = [[" " for _ in range(size_x)] for _ in range(size_y)]
for i in range(num_squares):
sol_x = solver.Value(x_starts[i])
sol_y = solver.Value(y_starts[i])
sol_s = solver.Value(sizes[i])
sol_x = solver.value(x_starts[i])
sol_y = solver.value(y_starts[i])
sol_s = solver.value(sizes[i])
char = format(i, "01x")
for j in range(sol_s):
for k in range(sol_s):

58
examples/python/cryptarithm_sat.py
View File

@@ -20,58 +20,58 @@ from ortools.sat.python import cp_model
def send_more_money():
"""Solve the cryptarithmic puzzle SEND+MORE=MONEY."""
"""solve the cryptarithmic puzzle SEND+MORE=MONEY."""
model = cp_model.CpModel()
# Create variables.
# Since s is a leading digit, it can't be 0.
s = model.NewIntVar(1, 9, "s")
e = model.NewIntVar(0, 9, "e")
n = model.NewIntVar(0, 9, "n")
d = model.NewIntVar(0, 9, "d")
s = model.new_int_var(1, 9, "s")
e = model.new_int_var(0, 9, "e")
n = model.new_int_var(0, 9, "n")
d = model.new_int_var(0, 9, "d")
# Since m is a leading digit, it can't be 0.
m = model.NewIntVar(1, 9, "m")
o = model.NewIntVar(0, 9, "o")
r = model.NewIntVar(0, 9, "r")
y = model.NewIntVar(0, 9, "y")
m = model.new_int_var(1, 9, "m")
o = model.new_int_var(0, 9, "o")
r = model.new_int_var(0, 9, "r")
y = model.new_int_var(0, 9, "y")
# Create carry variables. c0 is true if the first column of addends carries
# a 1, c2 is true if the second column carries a 1, and so on.
c0 = model.NewBoolVar("c0")
c1 = model.NewBoolVar("c1")
c2 = model.NewBoolVar("c2")
c3 = model.NewBoolVar("c3")
c0 = model.new_bool_var("c0")
c1 = model.new_bool_var("c1")
c2 = model.new_bool_var("c2")
c3 = model.new_bool_var("c3")
# Force all letters to take on different values.
model.AddAllDifferent(s, e, n, d, m, o, r, y)
model.add_all_different(s, e, n, d, m, o, r, y)
# Column 0:
model.Add(c0 == m)
model.add(c0 == m)
# Column 1:
model.Add(c1 + s + m == o + 10 * c0)
model.add(c1 + s + m == o + 10 * c0)
# Column 2:
model.Add(c2 + e + o == n + 10 * c1)
model.add(c2 + e + o == n + 10 * c1)
# Column 3:
model.Add(c3 + n + r == e + 10 * c2)
model.add(c3 + n + r == e + 10 * c2)
# Column 4:
model.Add(d + e == y + 10 * c3)
model.add(d + e == y + 10 * c3)
# Solve model.
# solve model.
solver = cp_model.CpSolver()
if solver.Solve(model) == cp_model.OPTIMAL:
if solver.solve(model) == cp_model.OPTIMAL:
print("Optimal solution found!")
print("s:", solver.Value(s))
print("e:", solver.Value(e))
print("n:", solver.Value(n))
print("d:", solver.Value(d))
print("m:", solver.Value(m))
print("o:", solver.Value(o))
print("r:", solver.Value(r))
print("y:", solver.Value(y))
print("s:", solver.value(s))
print("e:", solver.value(e))
print("n:", solver.value(n))
print("d:", solver.value(d))
print("m:", solver.value(m))
print("o:", solver.value(o))
print("r:", solver.value(r))
print("y:", solver.value(y))
def main(_):

56
examples/python/flexible_job_shop_sat.py
View File

@@ -41,13 +41,13 @@ class SolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Called at each new solution."""
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, self.WallTime(), self.ObjectiveValue())
% (self.__solution_count, self.wall_time, self.objective_value)
)
self.__solution_count += 1
def flexible_jobshop():
"""Solve a small flexible jobshop problem."""
"""solve a small flexible jobshop problem."""
# Data part.
jobs = [ # task = (processing_time, machine_id)
[ # Job 0
@@ -113,12 +113,12 @@ def flexible_jobshop():
# Create main interval for the task.
suffix_name = "_j%i_t%i" % (job_id, task_id)
start = model.NewIntVar(0, horizon, "start" + suffix_name)
duration = model.NewIntVar(
start = model.new_int_var(0, horizon, "start" + suffix_name)
duration = model.new_int_var(
min_duration, max_duration, "duration" + suffix_name
)
end = model.NewIntVar(0, horizon, "end" + suffix_name)
interval = model.NewIntervalVar(
end = model.new_int_var(0, horizon, "end" + suffix_name)
interval = model.new_interval_var(
start, duration, end, "interval" + suffix_name
)
@@ -127,7 +127,7 @@ def flexible_jobshop():
# Add precedence with previous task in the same job.
if previous_end is not None:
model.Add(start >= previous_end)
model.add(start >= previous_end)
previous_end = end
# Create alternative intervals.
@@ -135,19 +135,19 @@ def flexible_jobshop():
l_presences = []
for alt_id in all_alternatives:
alt_suffix = "_j%i_t%i_a%i" % (job_id, task_id, alt_id)
l_presence = model.NewBoolVar("presence" + alt_suffix)
l_start = model.NewIntVar(0, horizon, "start" + alt_suffix)
l_presence = model.new_bool_var("presence" + alt_suffix)
l_start = model.new_int_var(0, horizon, "start" + alt_suffix)
l_duration = task[alt_id][0]
l_end = model.NewIntVar(0, horizon, "end" + alt_suffix)
l_interval = model.NewOptionalIntervalVar(
l_end = model.new_int_var(0, horizon, "end" + alt_suffix)
l_interval = model.new_optional_interval_var(
l_start, l_duration, l_end, l_presence, "interval" + alt_suffix
)
l_presences.append(l_presence)
# Link the primary/global variables with the local ones.
model.Add(start == l_start).OnlyEnforceIf(l_presence)
model.Add(duration == l_duration).OnlyEnforceIf(l_presence)
model.Add(end == l_end).OnlyEnforceIf(l_presence)
model.add(start == l_start).only_enforce_if(l_presence)
model.add(duration == l_duration).only_enforce_if(l_presence)
model.add(end == l_end).only_enforce_if(l_presence)
# Add the local interval to the right machine.
intervals_per_resources[task[alt_id][1]].append(l_interval)
@@ -156,10 +156,10 @@ def flexible_jobshop():
presences[(job_id, task_id, alt_id)] = l_presence
# Select exactly one presence variable.
model.AddExactlyOne(l_presences)
model.add_exactly_one(l_presences)
else:
intervals_per_resources[task[0][1]].append(interval)
presences[(job_id, task_id, 0)] = model.NewConstant(1)
presences[(job_id, task_id, 0)] = model.new_constant(1)
job_ends.append(previous_end)
@@ -167,28 +167,28 @@ def flexible_jobshop():
for machine_id in all_machines:
intervals = intervals_per_resources[machine_id]
if len(intervals) > 1:
model.AddNoOverlap(intervals)
model.add_no_overlap(intervals)
# Makespan objective
makespan = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(makespan, job_ends)
model.Minimize(makespan)
makespan = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(makespan, job_ends)
model.minimize(makespan)
# Solve model.
solver = cp_model.CpSolver()
solution_printer = SolutionPrinter()
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
# Print final solution.
for job_id in all_jobs:
print("Job %i:" % job_id)
for task_id in range(len(jobs[job_id])):
start_value = solver.Value(starts[(job_id, task_id)])
start_value = solver.value(starts[(job_id, task_id)])
machine = -1
duration = -1
selected = -1
for alt_id in range(len(jobs[job_id][task_id])):
if solver.Value(presences[(job_id, task_id, alt_id)]):
if solver.value(presences[(job_id, task_id, alt_id)]):
duration = jobs[job_id][task_id][alt_id][0]
machine = jobs[job_id][task_id][alt_id][1]
selected = alt_id
@@ -197,12 +197,12 @@ def flexible_jobshop():
% (job_id, task_id, start_value, selected, machine, duration)
)
print("Solve status: %s" % solver.StatusName(status))
print("Optimal objective value: %i" % solver.ObjectiveValue())
print("solve status: %s" % solver.status_name(status))
print("Optimal objective value: %i" % solver.objective_value)
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
flexible_jobshop()

66
examples/python/gate_scheduling_sat.py
View File

@@ -67,66 +67,70 @@ def main(_):
for i in all_jobs:
# Create main interval.
start = model.NewIntVar(0, horizon, "start_%i" % i)
start = model.new_int_var(0, horizon, "start_%i" % i)
duration = jobs[i][0]
end = model.NewIntVar(0, horizon, "end_%i" % i)
interval = model.NewIntervalVar(start, duration, end, "interval_%i" % i)
end = model.new_int_var(0, horizon, "end_%i" % i)
interval = model.new_interval_var(start, duration, end, "interval_%i" % i)
starts.append(start)
intervals.append(interval)
ends.append(end)
demands.append(jobs[i][1])
# Create an optional copy of interval to be executed on machine 0.
performed_on_m0 = model.NewBoolVar("perform_%i_on_m0" % i)
performed_on_m0 = model.new_bool_var("perform_%i_on_m0" % i)
performed.append(performed_on_m0)
start0 = model.NewIntVar(0, horizon, "start_%i_on_m0" % i)
end0 = model.NewIntVar(0, horizon, "end_%i_on_m0" % i)
interval0 = model.NewOptionalIntervalVar(
start0 = model.new_int_var(0, horizon, "start_%i_on_m0" % i)
end0 = model.new_int_var(0, horizon, "end_%i_on_m0" % i)
interval0 = model.new_optional_interval_var(
start0, duration, end0, performed_on_m0, "interval_%i_on_m0" % i
)
intervals0.append(interval0)
# Create an optional copy of interval to be executed on machine 1.
start1 = model.NewIntVar(0, horizon, "start_%i_on_m1" % i)
end1 = model.NewIntVar(0, horizon, "end_%i_on_m1" % i)
interval1 = model.NewOptionalIntervalVar(
start1, duration, end1, performed_on_m0.Not(), "interval_%i_on_m1" % i
start1 = model.new_int_var(0, horizon, "start_%i_on_m1" % i)
end1 = model.new_int_var(0, horizon, "end_%i_on_m1" % i)
interval1 = model.new_optional_interval_var(
start1,
duration,
end1,
performed_on_m0.negated(),
"interval_%i_on_m1" % i,
)
intervals1.append(interval1)
# We only propagate the constraint if the tasks is performed on the machine.
model.Add(start0 == start).OnlyEnforceIf(performed_on_m0)
model.Add(start1 == start).OnlyEnforceIf(performed_on_m0.Not())
model.add(start0 == start).only_enforce_if(performed_on_m0)
model.add(start1 == start).only_enforce_if(performed_on_m0.negated())
# Width constraint (modeled as a cumulative)
model.AddCumulative(intervals, demands, max_width)
model.add_cumulative(intervals, demands, max_width)
# Choose which machine to perform the jobs on.
model.AddNoOverlap(intervals0)
model.AddNoOverlap(intervals1)
model.add_no_overlap(intervals0)
model.add_no_overlap(intervals1)
# Objective variable.
makespan = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(makespan, ends)
model.Minimize(makespan)
makespan = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(makespan, ends)
model.minimize(makespan)
# Symmetry breaking.
model.Add(performed[0] == 0)
model.add(performed[0] == 0)
# Solve model.
solver = cp_model.CpSolver()
solver.Solve(model)
solver.solve(model)
# Output solution.
if visualization.RunFromIPython():
output = visualization.SvgWrapper(solver.ObjectiveValue(), max_width, 40.0)
output.AddTitle("Makespan = %i" % solver.ObjectiveValue())
output = visualization.SvgWrapper(solver.objective_value, max_width, 40.0)
output.AddTitle("Makespan = %i" % solver.objective_value)
color_manager = visualization.ColorManager()
color_manager.SeedRandomColor(0)
for i in all_jobs:
performed_machine = 1 - solver.Value(performed[i])
start = solver.Value(starts[i])
performed_machine = 1 - solver.value(performed[i])
start = solver.value(starts[i])
d_x = jobs[i][0]
d_y = jobs[i][1]
s_y = performed_machine * (max_width - d_y)
@@ -139,17 +143,17 @@ def main(_):
output.Display()
else:
print("Solution")
print(" - makespan = %i" % solver.ObjectiveValue())
print(" - makespan = %i" % solver.objective_value)
for i in all_jobs:
performed_machine = 1 - solver.Value(performed[i])
start = solver.Value(starts[i])
performed_machine = 1 - solver.value(performed[i])
start = solver.value(starts[i])
print(
" - Job %i starts at %i on machine %i" % (i, start, performed_machine)
)
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
if __name__ == "__main__":

32
examples/python/golomb_sat.py
View File

@@ -38,7 +38,7 @@ _PARAMS = flags.DEFINE_string(
)
def solve_golomb_ruler(order, params):
def solve_golomb_ruler(order: int, params: str):
"""Solve the Golomb ruler problem."""
# Create the model.
model = cp_model.CpModel()
@@ -46,26 +46,26 @@ def solve_golomb_ruler(order, params):
var_max = order * order
all_vars = list(range(0, order))
marks = [model.NewIntVar(0, var_max, f"marks_{i}") for i in all_vars]
marks = [model.new_int_var(0, var_max, f"marks_{i}") for i in all_vars]
model.Add(marks[0] == 0)
model.add(marks[0] == 0)
for i in range(order - 2):
model.Add(marks[i + 1] > marks[i])
model.add(marks[i + 1] > marks[i])
diffs = []
for i in range(order - 1):
for j in range(i + 1, order):
diff = model.NewIntVar(0, var_max, f"diff [{j},{i}]")
model.Add(diff == marks[j] - marks[i])
diff = model.new_int_var(0, var_max, f"diff [{j},{i}]")
model.add(diff == marks[j] - marks[i])
diffs.append(diff)
model.AddAllDifferent(diffs)
model.add_all_different(diffs)
# symmetry breaking
if order > 2:
model.Add(marks[order - 1] - marks[order - 2] > marks[1] - marks[0])
model.add(marks[order - 1] - marks[order - 2] > marks[1] - marks[0])
# Objective
model.Minimize(marks[order - 1])
model.minimize(marks[order - 1])
# Solve the model.
solver = cp_model.CpSolver()
@@ -73,21 +73,21 @@ def solve_golomb_ruler(order, params):
text_format.Parse(params, solver.parameters)
solution_printer = cp_model.ObjectiveSolutionPrinter()
print(f"Golomb ruler(order={order})")
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
# Print solution.
print(f"status: {solver.StatusName(status)}")
print(f"status: {solver.status_name(status)}")
if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
for idx, var in enumerate(marks):
print(f"mark[{idx}]: {solver.Value(var)}")
intervals = [solver.Value(diff) for diff in diffs]
print(f"mark[{idx}]: {solver.value(var)}")
intervals = [solver.value(diff) for diff in diffs]
intervals.sort()
print(f"intervals: {intervals}")
print("Statistics:")
print(f"- conflicts: {solver.NumConflicts()}")
print(f"- branches : {solver.NumBranches()}")
print(f"- wall time: {solver.WallTime()}s\n")
print(f"- conflicts: {solver.num_conflicts}")
print(f"- branches : {solver.num_branches}")
print(f"- wall time: {solver.wall_time}s\n")
def main(argv: Sequence[str]) -> None:

43
examples/python/hidato_sat.py
View File

@@ -14,12 +14,13 @@
"""Solves the Hidato problem with the CP-SAT solver."""
from typing import Union
from absl import app
from ortools.sat.colab import visualization
from ortools.sat.python import cp_model
def build_pairs(rows, cols):
def build_pairs(rows: int, cols: int) -> list[tuple[int, int]]:
"""Build closeness pairs for consecutive numbers.
Build set of allowed pairs such that two consecutive numbers touch
@@ -48,7 +49,7 @@ def build_pairs(rows, cols):
return result
def print_solution(positions, rows, cols):
def print_solution(positions: list[int], rows: int, cols: int):
"""Print a current solution."""
# Create empty board.
board = []
@@ -63,7 +64,7 @@ def print_solution(positions, rows, cols):
print_matrix(board)
def print_matrix(game):
def print_matrix(game: list[list[int]]) -> None:
"""Pretty print of a matrix."""
rows = len(game)
cols = len(game[0])
@@ -77,7 +78,7 @@ def print_matrix(game):
print(line)
def build_puzzle(problem):
def build_puzzle(problem: int) -> Union[None, list[list[int]]]:
"""Build the problem from its index."""
#
# models, a 0 indicates an open cell which number is not yet known.
@@ -146,8 +147,8 @@ def build_puzzle(problem):
return puzzle
def solve_hidato(puzzle, index):
"""Solve the given hidato table."""
def solve_hidato(puzzle: list[list[int]], index: int):
"""solve the given hidato table."""
# Create the model.
model = cp_model.CpModel()
@@ -161,58 +162,58 @@ def solve_hidato(puzzle, index):
print_matrix(puzzle)
#
# declare variables
# Declare variables.
#
positions = [model.NewIntVar(0, r * c - 1, "p[%i]" % i) for i in range(r * c)]
positions = [model.new_int_var(0, r * c - 1, "p[%i]" % i) for i in range(r * c)]
#
# constraints
# Constraints.
#
model.AddAllDifferent(positions)
model.add_all_different(positions)
#
# Fill in the clues
# 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)
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 = build_pairs(r, c)
for k in range(0, r * c - 1):
model.AddAllowedAssignments([positions[k], positions[k + 1]], close_tuples)
model.add_allowed_assignments([positions[k], positions[k + 1]], close_tuples)
#
# solution and search
# Solution and search.
#
solver = cp_model.CpSolver()
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL:
if visualization.RunFromIPython():
output = visualization.SvgWrapper(10, r, 40.0)
for i, var in enumerate(positions):
val = solver.Value(var)
val = solver.value(var)
x = val % c
y = val // c
color = "white" if puzzle[y][x] == 0 else "lightgreen"
output.AddRectangle(x, r - y - 1, 1, 1, color, "black", str(i + 1))
output.AddTitle("Puzzle %i solved in %f s" % (index, solver.WallTime()))
output.AddTitle("Puzzle %i solved in %f s" % (index, solver.wall_time))
output.Display()
else:
print_solution(
[solver.Value(x) for x in positions],
[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 s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
def main(_):

36
examples/python/jobshop_ft06_distance_sat.py
View File

@@ -31,7 +31,7 @@ import collections
from ortools.sat.python import cp_model
def distance_between_jobs(x, y):
def distance_between_jobs(x: int, y: int) -> int:
"""Returns the distance between tasks of job x and tasks of job y."""
return abs(x - y)
@@ -73,10 +73,10 @@ def jobshop_ft06_distance():
all_tasks = {}
for i in all_jobs:
for j in all_machines:
start_var = model.NewIntVar(0, horizon, "start_%i_%i" % (i, j))
start_var = model.new_int_var(0, horizon, "start_%i_%i" % (i, j))
duration = durations[i][j]
end_var = model.NewIntVar(0, horizon, "end_%i_%i" % (i, j))
interval_var = model.NewIntervalVar(
end_var = model.new_int_var(0, horizon, "end_%i_%i" % (i, j))
interval_var = model.new_interval_var(
start_var, duration, end_var, "interval_%i_%i" % (i, j)
)
all_tasks[(i, j)] = task_type(
@@ -96,51 +96,51 @@ def jobshop_ft06_distance():
job_indices.append(j)
job_starts.append(all_tasks[(j, k)].start)
job_ends.append(all_tasks[(j, k)].end)
model.AddNoOverlap(job_intervals)
model.add_no_overlap(job_intervals)
arcs = []
for j1 in range(len(job_intervals)):
# Initial arc from the dummy node (0) to a task.
start_lit = model.NewBoolVar("%i is first job" % j1)
start_lit = model.new_bool_var("%i is first job" % j1)
arcs.append((0, j1 + 1, start_lit))
# Final arc from an arc to the dummy node.
arcs.append((j1 + 1, 0, model.NewBoolVar("%i is last job" % j1)))
arcs.append((j1 + 1, 0, model.new_bool_var("%i is last job" % j1)))
for j2 in range(len(job_intervals)):
if j1 == j2:
continue
lit = model.NewBoolVar("%i follows %i" % (j2, j1))
lit = model.new_bool_var("%i follows %i" % (j2, j1))
arcs.append((j1 + 1, j2 + 1, lit))
# We add the reified precedence to link the literal with the
# times of the two tasks.
min_distance = distance_between_jobs(j1, j2)
model.Add(job_starts[j2] >= job_ends[j1] + min_distance).OnlyEnforceIf(
lit
)
model.add(
job_starts[j2] >= job_ends[j1] + min_distance
).only_enforce_if(lit)
model.AddCircuit(arcs)
model.add_circuit(arcs)
# Precedences inside a job.
for i in all_jobs:
for j in range(0, machines_count - 1):
model.Add(all_tasks[(i, j + 1)].start >= all_tasks[(i, j)].end)
model.add(all_tasks[(i, j + 1)].start >= all_tasks[(i, j)].end)
# Makespan objective.
obj_var = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(
obj_var = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(
obj_var, [all_tasks[(i, machines_count - 1)].end for i in all_jobs]
)
model.Minimize(obj_var)
model.minimize(obj_var)
# Solve model.
solver = cp_model.CpSolver()
status = solver.Solve(model)
status = solver.solve(model)
# Output solution.
if status == cp_model.OPTIMAL:
print("Optimal makespan: %i" % solver.ObjectiveValue())
print("Optimal makespan: %i" % solver.objective_value)
jobshop_ft06_distance()

28
examples/python/jobshop_ft06_sat.py
View File

@@ -29,7 +29,7 @@ from ortools.sat.colab import visualization
from ortools.sat.python import cp_model
def jobshop_ft06():
def jobshop_ft06() -> None:
"""Solves the ft06 jobshop."""
# Creates the solver.
model = cp_model.CpModel()
@@ -66,10 +66,10 @@ def jobshop_ft06():
all_tasks = {}
for i in all_jobs:
for j in all_machines:
start_var = model.NewIntVar(0, horizon, "start_%i_%i" % (i, j))
start_var = model.new_int_var(0, horizon, "start_%i_%i" % (i, j))
duration = durations[i][j]
end_var = model.NewIntVar(0, horizon, "end_%i_%i" % (i, j))
interval_var = model.NewIntervalVar(
end_var = model.new_int_var(0, horizon, "end_%i_%i" % (i, j))
interval_var = model.new_interval_var(
start_var, duration, end_var, "interval_%i_%i" % (i, j)
)
all_tasks[(i, j)] = task_type(
@@ -85,35 +85,35 @@ def jobshop_ft06():
if machines[j][k] == i:
machines_jobs.append(all_tasks[(j, k)].interval)
machine_to_jobs[i] = machines_jobs
model.AddNoOverlap(machines_jobs)
model.add_no_overlap(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)].start >= all_tasks[(i, j)].end)
model.add(all_tasks[(i, j + 1)].start >= all_tasks[(i, j)].end)
# Makespan objective.
obj_var = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(
obj_var = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(
obj_var, [all_tasks[(i, machines_count - 1)].end for i in all_jobs]
)
model.Minimize(obj_var)
model.minimize(obj_var)
# Solve model.
# Solve the model.
solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
status = solver.Solve(model)
status = solver.solve(model)
# Output solution.
# Output the solution.
if status == cp_model.OPTIMAL:
if visualization.RunFromIPython():
starts = [
[solver.Value(all_tasks[(i, j)][0]) for j in all_machines]
[solver.value(all_tasks[(i, j)][0]) for j in all_machines]
for i in all_jobs
]
visualization.DisplayJobshop(starts, durations, machines, "FT06")
else:
print("Optimal makespan: %i" % solver.ObjectiveValue())
print("Optimal makespan: %i" % solver.objective_value)
jobshop_ft06()

39
examples/python/jobshop_with_maintenance_sat.py
View File

@@ -31,7 +31,7 @@ class SolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Called at each new solution."""
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, self.WallTime(), self.ObjectiveValue())
% (self.__solution_count, self.wall_time, self.objective_value)
)
self.__solution_count += 1
@@ -65,13 +65,14 @@ def jobshop_with_maintenance():
machine_to_intervals = collections.defaultdict(list)
for job_id, job in enumerate(jobs_data):
for task_id, task in enumerate(job):
for entry in enumerate(job):
task_id, task = entry
machine = task[0]
duration = task[1]
suffix = "_%i_%i" % (job_id, task_id)
start_var = model.NewIntVar(0, horizon, "start" + suffix)
end_var = model.NewIntVar(0, horizon, "end" + suffix)
interval_var = model.NewIntervalVar(
start_var = model.new_int_var(0, horizon, "start" + suffix)
end_var = model.new_int_var(0, horizon, "end" + suffix)
interval_var = model.new_interval_var(
start_var, duration, end_var, "interval" + suffix
)
all_tasks[job_id, task_id] = task_type(
@@ -80,31 +81,31 @@ def jobshop_with_maintenance():
machine_to_intervals[machine].append(interval_var)
# Add maintenance interval (machine 0 is not available on time {4, 5, 6, 7}).
machine_to_intervals[0].append(model.NewIntervalVar(4, 4, 8, "weekend_0"))
machine_to_intervals[0].append(model.new_interval_var(4, 4, 8, "weekend_0"))
# Create and add disjunctive constraints.
for machine in all_machines:
model.AddNoOverlap(machine_to_intervals[machine])
model.add_no_overlap(machine_to_intervals[machine])
# Precedences inside a job.
for job_id, job in enumerate(jobs_data):
for task_id in range(len(job) - 1):
model.Add(
model.add(
all_tasks[job_id, task_id + 1].start >= all_tasks[job_id, task_id].end
)
# Makespan objective.
obj_var = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(
obj_var = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(
obj_var,
[all_tasks[job_id, len(job) - 1].end for job_id, job in enumerate(jobs_data)],
)
model.Minimize(obj_var)
model.minimize(obj_var)
# Solve model.
solver = cp_model.CpSolver()
solution_printer = SolutionPrinter()
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
# Output solution.
if status == cp_model.OPTIMAL:
@@ -115,7 +116,7 @@ def jobshop_with_maintenance():
machine = task[0]
assigned_jobs[machine].append(
assigned_task_type(
start=solver.Value(all_tasks[job_id, task_id].start),
start=solver.value(all_tasks[job_id, task_id].start),
job=job_id,
index=task_id,
duration=task[1],
@@ -132,13 +133,13 @@ def jobshop_with_maintenance():
for assigned_task in assigned_jobs[machine]:
name = "job_%i_%i" % (assigned_task.job, assigned_task.index)
# Add spaces to output to align columns.
# add spaces to output to align columns.
sol_line_tasks += "%-10s" % name
start = assigned_task.start
duration = assigned_task.duration
sol_tmp = "[%i,%i]" % (start, start + duration)
# Add spaces to output to align columns.
# add spaces to output to align columns.
sol_line += "%-10s" % sol_tmp
sol_line += "\n"
@@ -147,12 +148,12 @@ def jobshop_with_maintenance():
output += sol_line
# Finally print the solution found.
print("Optimal Schedule Length: %i" % solver.ObjectiveValue())
print("Optimal Schedule Length: %i" % solver.objective_value)
print(output)
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
def main(argv: Sequence[str]) -> None:

167
examples/python/knapsack_2d_sat.py
View File

@@ -29,6 +29,7 @@ from google.protobuf import text_format
from ortools.sat.python import cp_model
_OUTPUT_PROTO = flags.DEFINE_string(
"output_proto", "", "Output file to write the cp_model proto to."
)
@@ -42,7 +43,7 @@ _MODEL = flags.DEFINE_string(
)
def build_data():
def build_data() -> tuple[pd.Series, int, int]:
"""Build the data frame."""
data = """
item width height available value color
@@ -70,8 +71,8 @@ def build_data():
return (data, max_height, max_width)
def solve_with_duplicate_items(data, max_height, max_width):
"""Solve the problem by building 2 items (rotated or not) for each item."""
def solve_with_duplicate_items(data: pd.Series, max_height: int, max_width: int):
"""solve the problem by building 2 items (rotated or not) for each item."""
# Derived data (expanded to individual items).
data_widths = data["width"].to_numpy()
data_heights = data["height"].to_numpy()
@@ -105,41 +106,47 @@ def solve_with_duplicate_items(data, max_height, max_width):
for i in range(num_items):
## Is the item used?
is_used.append(model.NewBoolVar(f"is_used{i}"))
is_used.append(model.new_bool_var(f"is_used{i}"))
## Item coordinates.
x_starts.append(model.NewIntVar(0, max_width, f"x_start{i}"))
x_ends.append(model.NewIntVar(0, max_width, f"x_end{i}"))
y_starts.append(model.NewIntVar(0, max_height, f"y_start{i}"))
y_ends.append(model.NewIntVar(0, max_height, f"y_end{i}"))
x_starts.append(model.new_int_var(0, max_width, f"x_start{i}"))
x_ends.append(model.new_int_var(0, max_width, f"x_end{i}"))
y_starts.append(model.new_int_var(0, max_height, f"y_start{i}"))
y_ends.append(model.new_int_var(0, max_height, f"y_end{i}"))
## Interval variables.
x_intervals.append(
model.NewIntervalVar(
x_starts[i], item_widths[i] * is_used[i], x_ends[i], f"x_interval{i}"
model.new_interval_var(
x_starts[i],
item_widths[i] * is_used[i],
x_ends[i],
f"x_interval{i}",
)
)
y_intervals.append(
model.NewIntervalVar(
y_starts[i], item_heights[i] * is_used[i], y_ends[i], f"y_interval{i}"
model.new_interval_var(
y_starts[i],
item_heights[i] * is_used[i],
y_ends[i],
f"y_interval{i}",
)
)
# Unused boxes are fixed at (0.0).
model.Add(x_starts[i] == 0).OnlyEnforceIf(is_used[i].Not())
model.Add(y_starts[i] == 0).OnlyEnforceIf(is_used[i].Not())
model.add(x_starts[i] == 0).only_enforce_if(is_used[i].negated())
model.add(y_starts[i] == 0).only_enforce_if(is_used[i].negated())
# Constraints.
## Only one of non-rotated/rotated pair can be used.
for i in range(num_data_items):
model.Add(is_used[i] + is_used[i + num_data_items] <= 1)
model.add(is_used[i] + is_used[i + num_data_items] <= 1)
## 2D no overlap.
model.AddNoOverlap2D(x_intervals, y_intervals)
model.add_no_overlap_2d(x_intervals, y_intervals)
## Objective.
model.Maximize(cp_model.LinearExpr.WeightedSum(is_used, item_values))
model.maximize(cp_model.LinearExpr.weighted_sum(is_used, item_values))
# Output proto to file.
if _OUTPUT_PROTO.value:
@@ -152,27 +159,29 @@ def solve_with_duplicate_items(data, max_height, max_width):
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
status = solver.Solve(model)
status = solver.solve(model)
# Report solution.
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
used = {i for i in range(num_items) if solver.BooleanValue(is_used[i])}
used = {i for i in range(num_items) if solver.boolean_value(is_used[i])}
data = pd.DataFrame(
{
"x_start": [solver.Value(x_starts[i]) for i in used],
"y_start": [solver.Value(y_starts[i]) for i in used],
"x_start": [solver.value(x_starts[i]) for i in used],
"y_start": [solver.value(y_starts[i]) for i in used],
"item_width": [item_widths[i] for i in used],
"item_height": [item_heights[i] for i in used],
"x_end": [solver.Value(x_ends[i]) for i in used],
"y_end": [solver.Value(y_ends[i]) for i in used],
"x_end": [solver.value(x_ends[i]) for i in used],
"y_end": [solver.value(y_ends[i]) for i in used],
"item_value": [item_values[i] for i in used],
}
)
print(data)
def solve_with_duplicate_optional_items(data, max_height, max_width):
"""Solve the problem by building 2 optional items (rotated or not) for each item."""
def solve_with_duplicate_optional_items(
data: pd.Series, max_height: int, max_width: int
):
"""solve the problem by building 2 optional items (rotated or not) for each item."""
# Derived data (expanded to individual items).
data_widths = data["width"].to_numpy()
data_heights = data["height"].to_numpy()
@@ -204,42 +213,42 @@ def solve_with_duplicate_optional_items(data, max_height, max_width):
for i in range(num_items):
## Is the item used?
is_used.append(model.NewBoolVar(f"is_used{i}"))
is_used.append(model.new_bool_var(f"is_used{i}"))
## Item coordinates.
x_starts.append(
model.NewIntVar(0, max_width - int(item_widths[i]), f"x_start{i}")
model.new_int_var(0, max_width - int(item_widths[i]), f"x_start{i}")
)
y_starts.append(
model.NewIntVar(0, max_height - int(item_heights[i]), f"y_start{i}")
model.new_int_var(0, max_height - int(item_heights[i]), f"y_start{i}")
)
## Interval variables.
x_intervals.append(
model.NewOptionalFixedSizeIntervalVar(
model.new_optional_fixed_size_interval_var(
x_starts[i], item_widths[i], is_used[i], f"x_interval{i}"
)
)
y_intervals.append(
model.NewOptionalFixedSizeIntervalVar(
model.new_optional_fixed_size_interval_var(
y_starts[i], item_heights[i], is_used[i], f"y_interval{i}"
)
)
# Unused boxes are fixed at (0.0).
model.Add(x_starts[i] == 0).OnlyEnforceIf(is_used[i].Not())
model.Add(y_starts[i] == 0).OnlyEnforceIf(is_used[i].Not())
model.add(x_starts[i] == 0).only_enforce_if(is_used[i].negated())
model.add(y_starts[i] == 0).only_enforce_if(is_used[i].negated())
# Constraints.
## Only one of non-rotated/rotated pair can be used.
for i in range(num_data_items):
model.Add(is_used[i] + is_used[i + num_data_items] <= 1)
model.add(is_used[i] + is_used[i + num_data_items] <= 1)
## 2D no overlap.
model.AddNoOverlap2D(x_intervals, y_intervals)
model.add_no_overlap_2d(x_intervals, y_intervals)
## Objective.
model.Maximize(cp_model.LinearExpr.WeightedSum(is_used, item_values))
model.maximize(cp_model.LinearExpr.weighted_sum(is_used, item_values))
# Output proto to file.
if _OUTPUT_PROTO.value:
@@ -247,32 +256,32 @@ def solve_with_duplicate_optional_items(data, max_height, max_width):
with open(_OUTPUT_PROTO.value, "w") as text_file:
text_file.write(str(model))
# Solve model.
# solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
status = solver.Solve(model)
status = solver.solve(model)
# Report solution.
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
used = {i for i in range(num_items) if solver.BooleanValue(is_used[i])}
used = {i for i in range(num_items) if solver.boolean_value(is_used[i])}
data = pd.DataFrame(
{
"x_start": [solver.Value(x_starts[i]) for i in used],
"y_start": [solver.Value(y_starts[i]) for i in used],
"x_start": [solver.value(x_starts[i]) for i in used],
"y_start": [solver.value(y_starts[i]) for i in used],
"item_width": [item_widths[i] for i in used],
"item_height": [item_heights[i] for i in used],
"x_end": [solver.Value(x_starts[i]) + item_widths[i] for i in used],
"y_end": [solver.Value(y_starts[i]) + item_heights[i] for i in used],
"x_end": [solver.value(x_starts[i]) + item_widths[i] for i in used],
"y_end": [solver.value(y_starts[i]) + item_heights[i] for i in used],
"item_value": [item_values[i] for i in used],
}
)
print(data)
def solve_with_rotations(data, max_height, max_width):
"""Solve the problem by rotating items."""
def solve_with_rotations(data: pd.Series, max_height: int, max_width: int):
"""solve the problem by rotating items."""
# Derived data (expanded to individual items).
data_widths = data["width"].to_numpy()
data_heights = data["height"].to_numpy()
@@ -301,25 +310,29 @@ def solve_with_rotations(data, max_height, max_width):
for i in range(num_items):
sizes = [0, int(item_widths[i]), int(item_heights[i])]
# X coordinates.
x_starts.append(model.NewIntVar(0, max_width, f"x_start{i}"))
x_starts.append(model.new_int_var(0, max_width, f"x_start{i}"))
x_sizes.append(
model.NewIntVarFromDomain(cp_model.Domain.FromValues(sizes), f"x_size{i}")
model.new_int_var_from_domain(
cp_model.Domain.FromValues(sizes), f"x_size{i}"
)
)
x_ends.append(model.NewIntVar(0, max_width, f"x_end{i}"))
x_ends.append(model.new_int_var(0, max_width, f"x_end{i}"))
# Y coordinates.
y_starts.append(model.NewIntVar(0, max_height, f"y_start{i}"))
y_starts.append(model.new_int_var(0, max_height, f"y_start{i}"))
y_sizes.append(
model.NewIntVarFromDomain(cp_model.Domain.FromValues(sizes), f"y_size{i}")
model.new_int_var_from_domain(
cp_model.Domain.FromValues(sizes), f"y_size{i}"
)
)
y_ends.append(model.NewIntVar(0, max_height, f"y_end{i}"))
y_ends.append(model.new_int_var(0, max_height, f"y_end{i}"))
## Interval variables
x_intervals.append(
model.NewIntervalVar(x_starts[i], x_sizes[i], x_ends[i], f"x_interval{i}")
model.new_interval_var(x_starts[i], x_sizes[i], x_ends[i], f"x_interval{i}")
)
y_intervals.append(
model.NewIntervalVar(y_starts[i], y_sizes[i], y_ends[i], f"y_interval{i}")
model.new_interval_var(y_starts[i], y_sizes[i], y_ends[i], f"y_interval{i}")
)
# is_used[i] == True if and only if item i is selected.
@@ -329,34 +342,34 @@ def solve_with_rotations(data, max_height, max_width):
## for each item, decide is unselected, no_rotation, rotated.
for i in range(num_items):
not_selected = model.NewBoolVar(f"not_selected_{i}")
no_rotation = model.NewBoolVar(f"no_rotation_{i}")
rotated = model.NewBoolVar(f"rotated_{i}")
not_selected = model.new_bool_var(f"not_selected_{i}")
no_rotation = model.new_bool_var(f"no_rotation_{i}")
rotated = model.new_bool_var(f"rotated_{i}")
### Exactly one state must be chosen.
model.AddExactlyOne(not_selected, no_rotation, rotated)
model.add_exactly_one(not_selected, no_rotation, rotated)
### Define height and width according to the state.
dim1 = item_widths[i]
dim2 = item_heights[i]
# Unused boxes are fixed at (0.0).
model.Add(x_sizes[i] == 0).OnlyEnforceIf(not_selected)
model.Add(y_sizes[i] == 0).OnlyEnforceIf(not_selected)
model.Add(x_starts[i] == 0).OnlyEnforceIf(not_selected)
model.Add(y_starts[i] == 0).OnlyEnforceIf(not_selected)
model.add(x_sizes[i] == 0).only_enforce_if(not_selected)
model.add(y_sizes[i] == 0).only_enforce_if(not_selected)
model.add(x_starts[i] == 0).only_enforce_if(not_selected)
model.add(y_starts[i] == 0).only_enforce_if(not_selected)
# Sizes are fixed by the rotation.
model.Add(x_sizes[i] == dim1).OnlyEnforceIf(no_rotation)
model.Add(y_sizes[i] == dim2).OnlyEnforceIf(no_rotation)
model.Add(x_sizes[i] == dim2).OnlyEnforceIf(rotated)
model.Add(y_sizes[i] == dim1).OnlyEnforceIf(rotated)
model.add(x_sizes[i] == dim1).only_enforce_if(no_rotation)
model.add(y_sizes[i] == dim2).only_enforce_if(no_rotation)
model.add(x_sizes[i] == dim2).only_enforce_if(rotated)
model.add(y_sizes[i] == dim1).only_enforce_if(rotated)
is_used.append(not_selected.Not())
is_used.append(not_selected.negated())
## 2D no overlap.
model.AddNoOverlap2D(x_intervals, y_intervals)
model.add_no_overlap_2d(x_intervals, y_intervals)
# Objective.
model.Maximize(cp_model.LinearExpr.WeightedSum(is_used, item_values))
model.maximize(cp_model.LinearExpr.weighted_sum(is_used, item_values))
# Output proto to file.
if _OUTPUT_PROTO.value:
@@ -364,24 +377,24 @@ def solve_with_rotations(data, max_height, max_width):
with open(_OUTPUT_PROTO.value, "w") as text_file:
text_file.write(str(model))
# Solve model.
# solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
status = solver.Solve(model)
status = solver.solve(model)
# Report solution.
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
used = {i for i in range(num_items) if solver.BooleanValue(is_used[i])}
used = {i for i in range(num_items) if solver.boolean_value(is_used[i])}
data = pd.DataFrame(
{
"x_start": [solver.Value(x_starts[i]) for i in used],
"y_start": [solver.Value(y_starts[i]) for i in used],
"item_width": [solver.Value(x_sizes[i]) for i in used],
"item_height": [solver.Value(y_sizes[i]) for i in used],
"x_end": [solver.Value(x_ends[i]) for i in used],
"y_end": [solver.Value(y_ends[i]) for i in used],
"x_start": [solver.value(x_starts[i]) for i in used],
"y_start": [solver.value(y_starts[i]) for i in used],
"item_width": [solver.value(x_sizes[i]) for i in used],
"item_height": [solver.value(y_sizes[i]) for i in used],
"x_end": [solver.value(x_ends[i]) for i in used],
"y_end": [solver.value(y_ends[i]) for i in used],
"item_value": [item_values[i] for i in used],
}
)
@@ -389,7 +402,7 @@ def solve_with_rotations(data, max_height, max_width):
def main(_):
"""Solve the problem with all models."""
"""solve the problem with all models."""
data, max_height, max_width = build_data()
if _MODEL.value == "duplicate":
solve_with_duplicate_items(data, max_height, max_width)

72
examples/python/line_balancing_sat.py
View File

@@ -184,7 +184,7 @@ def solve_model_greedily(model):
def solve_boolean_model(model, hint):
"""Solve the given model."""
"""solve the given model."""
print("Solving using the Boolean model")
# Model data
@@ -207,73 +207,73 @@ def solve_boolean_model(model, hint):
# Create the variables
for t in all_tasks:
for p in all_pods:
assign[t, p] = model.NewBoolVar(f"assign_{t}_{p}")
possible[t, p] = model.NewBoolVar(f"possible_{t}_{p}")
assign[t, p] = model.new_bool_var(f"assign_{t}_{p}")
possible[t, p] = model.new_bool_var(f"possible_{t}_{p}")
# active[p] indicates if pod p is active.
active = [model.NewBoolVar(f"active_{p}") for p in all_pods]
active = [model.new_bool_var(f"active_{p}") for p in all_pods]
# Each task is done on exactly one pod.
for t in all_tasks:
model.AddExactlyOne([assign[t, p] for p in all_pods])
model.add_exactly_one([assign[t, p] for p in all_pods])
# Total tasks assigned to one pod cannot exceed cycle time.
for p in all_pods:
model.Add(sum(assign[t, p] * durations[t] for t in all_tasks) <= cycle_time)
model.add(sum(assign[t, p] * durations[t] for t in all_tasks) <= cycle_time)
# Maintain the possible variables:
# possible at pod p -> possible at any pod after p
for t in all_tasks:
for p in range(num_pods - 1):
model.AddImplication(possible[t, p], possible[t, p + 1])
model.add_implication(possible[t, p], possible[t, p + 1])
# Link possible and active variables.
for t in all_tasks:
for p in all_pods:
model.AddImplication(assign[t, p], possible[t, p])
model.add_implication(assign[t, p], possible[t, p])
if p > 1:
model.AddImplication(assign[t, p], possible[t, p - 1].Not())
model.add_implication(assign[t, p], possible[t, p - 1].negated())
# Precedences.
for before, after in precedences:
for p in range(1, num_pods):
model.AddImplication(assign[before, p], possible[after, p - 1].Not())
model.add_implication(assign[before, p], possible[after, p - 1].negated())
# Link active variables with the assign one.
for p in all_pods:
all_assign_vars = [assign[t, p] for t in all_tasks]
for a in all_assign_vars:
model.AddImplication(a, active[p])
model.AddBoolOr(all_assign_vars + [active[p].Not()])
model.add_implication(a, active[p])
model.add_bool_or(all_assign_vars + [active[p].negated()])
# Force pods to be contiguous. This is critical to get good lower bounds
# on the objective, even if it makes feasibility harder.
for p in range(1, num_pods):
model.AddImplication(active[p - 1].Not(), active[p].Not())
model.add_implication(active[p - 1].negated(), active[p].negated())
for t in all_tasks:
model.AddImplication(active[p].Not(), possible[t, p - 1])
model.add_implication(active[p].negated(), possible[t, p - 1])
# Objective.
model.Minimize(sum(active))
model.minimize(sum(active))
# Add search hinting from the greedy solution.
# add search hinting from the greedy solution.
for t in all_tasks:
model.AddHint(assign[t, hint[t]], 1)
model.add_hint(assign[t, hint[t]], 1)
if _OUTPUT_PROTO.value:
print(f"Writing proto to {_OUTPUT_PROTO.value}")
model.ExportToFile(_OUTPUT_PROTO.value)
model.export_to_file(_OUTPUT_PROTO.value)
# Solve model.
# solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
solver.parameters.log_search_progress = True
solver.Solve(model)
solver.solve(model)
def solve_scheduling_model(model, hint):
"""Solve the given model using a cumutive model."""
"""solve the given model using a cumutive model."""
print("Solving using the scheduling model")
# Model data
@@ -290,47 +290,49 @@ def solve_scheduling_model(model, hint):
# pod[t] indicates on which pod the task is performed.
pods = {}
for t in all_tasks:
pods[t] = model.NewIntVar(0, num_pods - 1, f"pod_{t}")
pods[t] = model.new_int_var(0, num_pods - 1, f"pod_{t}")
# Create the variables
intervals = []
demands = []
for t in all_tasks:
interval = model.NewFixedSizeIntervalVar(pods[t], 1, "")
interval = model.new_fixed_size_interval_var(pods[t], 1, "")
intervals.append(interval)
demands.append(durations[t])
# Add terminating interval as the objective.
obj_var = model.NewIntVar(1, num_pods, "obj_var")
obj_size = model.NewIntVar(1, num_pods, "obj_duration")
obj_interval = model.NewIntervalVar(obj_var, obj_size, num_pods + 1, "obj_interval")
# add terminating interval as the objective.
obj_var = model.new_int_var(1, num_pods, "obj_var")
obj_size = model.new_int_var(1, num_pods, "obj_duration")
obj_interval = model.new_interval_var(
obj_var, obj_size, num_pods + 1, "obj_interval"
)
intervals.append(obj_interval)
demands.append(cycle_time)
# Cumulative constraint.
model.AddCumulative(intervals, demands, cycle_time)
model.add_cumulative(intervals, demands, cycle_time)
# Precedences.
for before, after in precedences:
model.Add(pods[after] >= pods[before])
model.add(pods[after] >= pods[before])
# Objective.
model.Minimize(obj_var)
model.minimize(obj_var)
# Add search hinting from the greedy solution.
# add search hinting from the greedy solution.
for t in all_tasks:
model.AddHint(pods[t], hint[t])
model.add_hint(pods[t], hint[t])
if _OUTPUT_PROTO.value:
print(f"Writing proto to{_OUTPUT_PROTO.value}")
model.ExportToFile(_OUTPUT_PROTO.value)
model.export_to_file(_OUTPUT_PROTO.value)
# Solve model.
# solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
solver.parameters.log_search_progress = True
solver.Solve(model)
solver.solve(model)
def main(argv: Sequence[str]) -> None:

20
examples/python/maze_escape_sat.py Executable file → Normal file
View File

@@ -50,8 +50,8 @@ def add_neighbor(size, x, y, z, dx, dy, dz, model, index_map, position_to_rank,
before_rank = position_to_rank[(x, y, z)]
after_index = index_map[(x + dx, y + dy, z + dz)]
after_rank = position_to_rank[(x + dx, y + dy, z + dz)]
move_literal = model.NewBoolVar("")
model.Add(after_rank == before_rank + 1).OnlyEnforceIf(move_literal)
move_literal = model.new_bool_var("")
model.add(after_rank == before_rank + 1).only_enforce_if(move_literal)
arcs.append((before_index, after_index, move_literal))
@@ -79,13 +79,13 @@ def escape_the_maze(params, output_proto):
position_to_rank = {}
for coord in reverse_map:
position_to_rank[coord] = model.NewIntVar(0, counter - 1, f"rank_{coord}")
position_to_rank[coord] = model.new_int_var(0, counter - 1, f"rank_{coord}")
# Path constraints.
model.Add(position_to_rank[start] == 0)
model.Add(position_to_rank[end] == counter - 1)
model.add(position_to_rank[start] == 0)
model.add(position_to_rank[end] == counter - 1)
for i in range(len(boxes) - 1):
model.Add(position_to_rank[boxes[i]] < position_to_rank[boxes[i + 1]])
model.add(position_to_rank[boxes[i]] < position_to_rank[boxes[i + 1]])
# Circuit constraint: visit all blocks exactly once, and maintains the rank
# of each block.
@@ -116,18 +116,18 @@ def escape_the_maze(params, output_proto):
arcs.append((index_map[end], index_map[start], True))
# Adds the circuit (hamiltonian path) constraint.
model.AddCircuit(arcs)
model.add_circuit(arcs)
# Exports the model if required.
if output_proto:
model.ExportToFile(output_proto)
model.export_to_file(output_proto)
# Solve model.
solver = cp_model.CpSolver()
if params:
text_format.Parse(params, solver.parameters)
solver.parameters.log_search_progress = True
result = solver.Solve(model)
result = solver.solve(model)
# Prints solution.
if result == cp_model.OPTIMAL:
@@ -136,7 +136,7 @@ def escape_the_maze(params, output_proto):
for y in range(size):
for z in range(size):
position = (x, y, z)
rank = solver.Value(position_to_rank[position])
rank = solver.value(position_to_rank[position])
msg = f"({x}, {y}, {z})"
if position == start:
msg += " [start]"

179
examples/python/memory_layout_and_infeasibility_sat.py Normal file
View File

@@ -0,0 +1,179 @@
#!/usr/bin/env python3
# Copyright 2010-2022 Google LLC
# 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.
"""Solves the memory allocation problem, and returns a minimal set of demands to explain infeasibility."""
from collections.abc import Sequence
from typing import List
from absl import app
from absl import flags
from google.protobuf import text_format
from ortools.sat.python import cp_model
_OUTPUT_PROTO = flags.DEFINE_string(
"output_proto", "", "Output file to write the cp_model proto to."
)
_PARAMS = flags.DEFINE_string(
"params", "num_workers:1,linearization_level:2", "Sat solver parameters."
)
# Input of the problem.
DEMANDS = [
[1578, 1583, 43008, 1],
[1588, 1589, 11264, 1],
[1590, 1595, 43008, 1],
[1583, 1588, 47872, 1],
[1589, 1590, 22848, 1],
[1586, 1590, 22848, 1],
[1591, 1594, 43008, 1],
]
CAPACITY = 98304
def solve_hard_model(output_proto: str, params: str) -> bool:
"""Solves the hard assignment model."""
print("Solving the hard assignment model")
model = cp_model.CpModel()
x_intervals: List[cp_model.IntervalVar] = []
y_starts: List[cp_model.IntVar] = []
y_intervals: List[cp_model.IntervalVar] = []
for start, end, demand, unused_alignment in DEMANDS:
x_interval = model.new_fixed_size_interval_var(start, end - start + 1, "")
y_start = model.new_int_var(0, CAPACITY - demand, "")
y_interval = model.new_fixed_size_interval_var(y_start, demand, "")
x_intervals.append(x_interval)
y_starts.append(y_start)
y_intervals.append(y_interval)
model.add_no_overlap_2d(x_intervals, y_intervals)
if output_proto:
model.export_to_file(output_proto)
solver = cp_model.CpSolver()
if params:
text_format.Parse(params, solver.parameters)
status = solver.solve(model)
print(solver.response_stats())
if status == cp_model.FEASIBLE or status == cp_model.OPTIMAL:
for index, start in enumerate(y_starts):
print(f"task {index} buffer starts at {solver.value(start)}")
return status != cp_model.INFEASIBLE
def solve_soft_model_with_assumptions() -> None:
"""Solves the soft model using assumptions."""
print("Solving the soft model using assumptions")
model = cp_model.CpModel()
presences: List[cp_model.IntVar] = []
x_intervals: List[cp_model.IntervalVar] = []
y_starts: List[cp_model.IntVar] = []
y_intervals: List[cp_model.IntervalVar] = []
for start, end, demand, unused_alignment in DEMANDS:
presence = model.new_bool_var("")
x_interval = model.new_optional_fixed_size_interval_var(
start, end - start + 1, presence, ""
)
y_start = model.new_int_var(0, CAPACITY - demand, "")
y_interval = model.new_optional_fixed_size_interval_var(
y_start, demand, presence, ""
)
presences.append(presence)
x_intervals.append(x_interval)
y_starts.append(y_start)
y_intervals.append(y_interval)
model.add_no_overlap_2d(x_intervals, y_intervals)
model.add_assumptions(presences)
solver = cp_model.CpSolver()
status = solver.solve(model)
print(solver.response_stats())
if status == cp_model.INFEASIBLE:
# The list actually contains the indices of the variables sufficient to
# explain infeasibility.
infeasible_variable_indices = solver.sufficient_assumptions_for_infeasibility()
infeasible_variable_indices_set = set(infeasible_variable_indices)
for index, presence in enumerate(presences):
if presence.index in infeasible_variable_indices_set:
print(f"using task {index} is sufficient to explain infeasibility")
def solve_soft_model_with_maximization(params: str) -> None:
"""Solves the soft model using maximization."""
print("Solving the soft model using minimization")
model = cp_model.CpModel()
presences: List[cp_model.IntVar] = []
x_intervals: List[cp_model.IntervalVar] = []
y_starts: List[cp_model.IntVar] = []
y_intervals: List[cp_model.IntervalVar] = []
for start, end, demand, unused_alignment in DEMANDS:
presence = model.new_bool_var("")
x_interval = model.new_optional_fixed_size_interval_var(
start, end - start + 1, presence, ""
)
y_start = model.new_int_var(0, CAPACITY - demand, "")
y_interval = model.new_optional_fixed_size_interval_var(
y_start, demand, presence, ""
)
presences.append(presence)
x_intervals.append(x_interval)
y_starts.append(y_start)
y_intervals.append(y_interval)
model.add_no_overlap_2d(x_intervals, y_intervals)
model.maximize(sum(presences))
solver = cp_model.CpSolver()
if params:
text_format.Parse(params, solver.parameters)
status = solver.solve(model)
print(solver.response_stats())
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
for index, presence in enumerate(presences):
if not solver.boolean_value(presence):
print(f"task {index} does not fit")
else:
print(f"task {index} buffer starts at {solver.value(y_starts[index])}")
def main(argv: Sequence[str]) -> None:
if len(argv) > 1:
raise app.UsageError("Too many command-line arguments.")
if not solve_hard_model(_OUTPUT_PROTO.value, _PARAMS.value):
solve_soft_model_with_assumptions()
solve_soft_model_with_maximization(_PARAMS.value)
if __name__ == "__main__":
app.run(main)

24
examples/python/no_wait_baking_scheduling_sat.py Executable file → Normal file
View File

@@ -232,68 +232,68 @@ def solve_with_cp_sat(recipes, resources, orders):
start = None
if previous_end is None:
start = model.NewIntVar(start_work, horizon, f"start{suffix}")
start = model.new_int_var(start_work, horizon, f"start{suffix}")
orders_sequence_of_events[order_id].append(
(start, f"start{suffix}")
)
else:
start = previous_end
size = model.NewIntVar(
size = model.new_int_var(
task.min_duration, task.max_duration, f"size{suffix}"
)
end = None
if task == recipe.tasks[-1]:
# The order must end after the due_date. Ideally, exactly at the
# due_date.
tardiness = model.NewIntVar(0, horizon - due_date, f"end{suffix}")
tardiness = model.new_int_var(0, horizon - due_date, f"end{suffix}")
end = tardiness + due_date
# Store the end_var for the objective.
tardiness_vars.append(tardiness)
else:
end = model.NewIntVar(start_work, horizon, f"end{suffix}")
end = model.new_int_var(start_work, horizon, f"end{suffix}")
orders_sequence_of_events[order_id].append((end, f"end{suffix}"))
previous_end = end
# Per resource copy.
presence_literals = []
for resource in resource_list_by_skill_name[skill_name]:
presence = model.NewBoolVar(f"presence{suffix}_{resource.name}")
copy = model.NewOptionalIntervalVar(
presence = model.new_bool_var(f"presence{suffix}_{resource.name}")
copy = model.new_optional_interval_var(
start, size, end, presence, f"interval{suffix}_{resource.name}"
)
interval_list_by_resource_name[resource.name].append(copy)
presence_literals.append(presence)
# Only one copy will be performed.
model.AddExactlyOne(presence_literals)
model.add_exactly_one(presence_literals)
# Create resource constraints.
for resource in resources:
intervals = interval_list_by_resource_name[resource.name]
if resource.capacity == 1:
model.AddNoOverlap(intervals)
model.add_no_overlap(intervals)
else:
model.AddCumulative(intervals, [1] * len(intervals), resource.capacity)
model.add_cumulative(intervals, [1] * len(intervals), resource.capacity)
# The objective is to minimize the sum of the tardiness values of each jobs.
# The tardiness is difference between the end time of an order and its
# due date.
model.Minimize(sum(tardiness_vars))
model.minimize(sum(tardiness_vars))
# Solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
solver.parameters.log_search_progress = True
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
for order_id in sorted_orders:
print(f"{order_id}:")
for time_expr, event_id in orders_sequence_of_events[order_id]:
time = solver.Value(time_expr)
time = solver.value(time_expr)
print(f" {event_id} at {time // 60}:{time % 60:02}")

39
examples/python/nqueens_sat.py
View File

@@ -26,16 +26,17 @@ _SIZE = flags.DEFINE_integer("size", 8, "Number of queens.")
class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, queens):
def __init__(self, queens: list[cp_model.IntVar]):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__queens = queens
self.__solution_count = 0
self.__start_time = time.time()
def SolutionCount(self):
@property
def solution_count(self) -> int:
return self.__solution_count
def on_solution_callback(self):
def on_solution_callback(self) -> None:
current_time = time.time()
print(
"Solution %i, time = %f s"
@@ -46,7 +47,7 @@ class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback):
all_queens = range(len(self.__queens))
for i in all_queens:
for j in all_queens:
if self.Value(self.__queens[j]) == i:
if self.value(self.__queens[j]) == i:
# There is a queen in column j, row i.
print("Q", end=" ")
else:
@@ -63,41 +64,43 @@ def main(_):
### Creates the variables.
# The array index is the column, and the value is the row.
queens = [model.NewIntVar(0, board_size - 1, "x%i" % i) for i in range(board_size)]
queens = [
model.new_int_var(0, board_size - 1, "x%i" % i) for i in range(board_size)
]
### Creates the constraints.
# All columns must be different because the indices of queens are all
# different, so we just add the all different constraint on the rows.
model.AddAllDifferent(queens)
model.add_all_different(queens)
# No two queens can be on the same diagonal.
diag1 = []
diag2 = []
for i in range(board_size):
q1 = model.NewIntVar(0, 2 * board_size, "diag1_%i" % i)
q2 = model.NewIntVar(-board_size, board_size, "diag2_%i" % i)
q1 = model.new_int_var(0, 2 * board_size, "diag1_%i" % i)
q2 = model.new_int_var(-board_size, board_size, "diag2_%i" % i)
diag1.append(q1)
diag2.append(q2)
model.Add(q1 == queens[i] + i)
model.Add(q2 == queens[i] - i)
model.AddAllDifferent(diag1)
model.AddAllDifferent(diag2)
model.add(q1 == queens[i] + i)
model.add(q2 == queens[i] - i)
model.add_all_different(diag1)
model.add_all_different(diag2)
### Solve model.
solver = cp_model.CpSolver()
solution_printer = NQueenSolutionPrinter(queens)
# Enumerate all solutions.
solver.parameters.enumerate_all_solutions = True
# Solve.
solver.Solve(model, solution_printer)
# solve.
solver.solve(model, solution_printer)
print()
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - solutions found : %i" % solution_printer.SolutionCount())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
print(" - solutions found : %i" % solution_printer.solution_count)
if __name__ == "__main__":

31
examples/python/prize_collecting_tsp_sat.py Executable file → Normal file
View File

@@ -71,14 +71,19 @@ VISIT_VALUES[0] = 0
# Create a console solution printer.
def print_solution(solver, visited_nodes, used_arcs, num_nodes):
def print_solution(
solver: cp_model.CpSolver,
visited_nodes: list[cp_model.IntVar],
used_arcs: dict[tuple[int, int], cp_model.IntVar],
num_nodes: int,
) -> None:
"""Prints solution on console."""
# Display dropped nodes.
dropped_nodes = "Dropped nodes:"
for i in range(num_nodes):
if i == 0:
continue
if not solver.BooleanValue(visited_nodes[i]):
if not solver.boolean_value(visited_nodes[i]):
dropped_nodes += f" {i}({VISIT_VALUES[i]})"
print(dropped_nodes)
# Display routes
@@ -94,7 +99,7 @@ def print_solution(solver, visited_nodes, used_arcs, num_nodes):
for node in range(num_nodes):
if node == current_node:
continue
if solver.BooleanValue(used_arcs[current_node, node]):
if solver.boolean_value(used_arcs[current_node, node]):
route_distance += DISTANCE_MATRIX[current_node][node]
current_node = node
if current_node == 0:
@@ -102,7 +107,7 @@ def print_solution(solver, visited_nodes, used_arcs, num_nodes):
break
plan_output += f" {current_node}\n"
plan_output += f"Distance of the route: {route_distance}m\n"
plan_output += f"Value collected: {value_collected}/{sum(VISIT_VALUES)}\n"
plan_output += f"value collected: {value_collected}/{sum(VISIT_VALUES)}\n"
print(plan_output)
@@ -123,8 +128,8 @@ def prize_collecting_tsp():
# Create the circuit constraint.
arcs = []
for i in all_nodes:
is_visited = model.NewBoolVar(f"{i} is visited")
arcs.append((i, i, is_visited.Not()))
is_visited = model.new_bool_var(f"{i} is visited")
arcs.append((i, i, is_visited.negated()))
obj_vars.append(is_visited)
obj_coeffs.append(VISIT_VALUES[i])
@@ -132,22 +137,22 @@ def prize_collecting_tsp():
for j in all_nodes:
if i == j:
used_arcs[i, j] = is_visited.Not()
used_arcs[i, j] = is_visited.negated()
continue
arc_is_used = model.NewBoolVar(f"{j} follows {i}")
arc_is_used = model.new_bool_var(f"{j} follows {i}")
arcs.append((i, j, arc_is_used))
obj_vars.append(arc_is_used)
obj_coeffs.append(-DISTANCE_MATRIX[i][j])
used_arcs[i, j] = arc_is_used
model.AddCircuit(arcs)
model.add_circuit(arcs)
# Node 0 must be visited.
model.Add(visited_nodes[0] == 1)
model.add(visited_nodes[0] == 1)
# limit the route distance
model.Add(
model.add(
sum(
used_arcs[i, j] * DISTANCE_MATRIX[i][j]
for i in all_nodes
@@ -157,7 +162,7 @@ def prize_collecting_tsp():
)
# Maximize visited node values minus the travelled distance.
model.Maximize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
model.maximize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
# Solve and print out the solution.
solver = cp_model.CpSolver()
@@ -166,7 +171,7 @@ def prize_collecting_tsp():
solver.parameters.num_search_workers = 8
solver.parameters.log_search_progress = True
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.FEASIBLE or status == cp_model.OPTIMAL:
print_solution(solver, visited_nodes, used_arcs, num_nodes)

36
examples/python/prize_collecting_vrp_sat.py Executable file → Normal file
View File

@@ -71,7 +71,13 @@ VISIT_VALUES[0] = 0
# Create a console solution printer.
def print_solution(solver, visited_nodes, used_arcs, num_nodes, num_vehicles):
def print_solution(
solver: cp_model.CpSolver,
visited_nodes: dict[int, list[cp_model.IntVar]],
used_arcs: dict[int, dict[tuple[int, int], cp_model.IntVar]],
num_nodes: int,
num_vehicles: int,
) -> None:
"""Prints solution on console."""
# Display dropped nodes.
dropped_nodes = "Dropped nodes:"
@@ -79,7 +85,7 @@ def print_solution(solver, visited_nodes, used_arcs, num_nodes, num_vehicles):
if node == 0:
continue
is_visited = sum(
[solver.BooleanValue(visited_nodes[v][node]) for v in range(num_vehicles)]
[solver.boolean_value(visited_nodes[v][node]) for v in range(num_vehicles)]
)
if not is_visited:
dropped_nodes += f" {node}({VISIT_VALUES[node]})"
@@ -100,7 +106,7 @@ def print_solution(solver, visited_nodes, used_arcs, num_nodes, num_vehicles):
for node in range(num_nodes):
if node == current_node:
continue
if solver.BooleanValue(used_arcs[v][current_node, node]):
if solver.boolean_value(used_arcs[v][current_node, node]):
route_distance += DISTANCE_MATRIX[current_node][node]
current_node = node
if current_node == 0:
@@ -108,12 +114,12 @@ def print_solution(solver, visited_nodes, used_arcs, num_nodes, num_vehicles):
break
plan_output += f" {current_node}\n"
plan_output += f"Distance of the route: {route_distance}m\n"
plan_output += f"Value collected: {value_collected}\n"
plan_output += f"value collected: {value_collected}\n"
print(plan_output)
total_distance += route_distance
total_value_collected += value_collected
print(f"Total Distance: {total_distance}m")
print(f"Total Value collected: {total_value_collected}/{sum(VISIT_VALUES)}")
print(f"Total value collected: {total_value_collected}/{sum(VISIT_VALUES)}")
def prize_collecting_vrp():
@@ -137,8 +143,8 @@ def prize_collecting_vrp():
used_arcs[v] = {}
arcs = []
for i in all_nodes:
is_visited = model.NewBoolVar(f"{i} is visited")
arcs.append((i, i, is_visited.Not()))
is_visited = model.new_bool_var(f"{i} is visited")
arcs.append((i, i, is_visited.negated()))
obj_vars.append(is_visited)
obj_coeffs.append(VISIT_VALUES[i])
@@ -146,22 +152,22 @@ def prize_collecting_vrp():
for j in all_nodes:
if i == j:
used_arcs[v][i, j] = is_visited.Not()
used_arcs[v][i, j] = is_visited.negated()
continue
arc_is_used = model.NewBoolVar(f"{j} follows {i}")
arc_is_used = model.new_bool_var(f"{j} follows {i}")
arcs.append((i, j, arc_is_used))
obj_vars.append(arc_is_used)
obj_coeffs.append(-DISTANCE_MATRIX[i][j])
used_arcs[v][i, j] = arc_is_used
model.AddCircuit(arcs)
model.add_circuit(arcs)
# Node 0 must be visited.
model.Add(visited_nodes[v][0] == 1)
model.add(visited_nodes[v][0] == 1)
# limit the route distance
model.Add(
model.add(
sum(
used_arcs[v][i, j] * DISTANCE_MATRIX[i][j]
for i in all_nodes
@@ -172,10 +178,10 @@ def prize_collecting_vrp():
# Each node is visited at most once
for node in range(1, num_nodes):
model.AddAtMostOne([visited_nodes[v][node] for v in range(num_vehicles)])
model.add_at_most_one([visited_nodes[v][node] for v in range(num_vehicles)])
# Maximize visited node values minus the travelled distance.
model.Maximize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
model.maximize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
# Solve and print out the solution.
solver = cp_model.CpSolver()
@@ -183,7 +189,7 @@ def prize_collecting_vrp():
solver.parameters.max_time_in_seconds = 15.0
solver.parameters.log_search_progress = True
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.FEASIBLE or status == cp_model.OPTIMAL:
print_solution(solver, visited_nodes, used_arcs, num_nodes, num_vehicles)

4
examples/python/proto_solve.py
View File

@@ -20,7 +20,7 @@ def main(_):
# Create solver.
solver = model_builder.ModelSolver(_SOLVER.value)
if not solver:
if not solver.solver_is_supported():
print(f'Cannot create solver with name \'{_SOLVER.value}\'')
return
@@ -36,4 +36,4 @@ def main(_):
if __name__ == '__main__':
app.run(main)
app.run(main)

18
examples/python/qubo_sat.py
View File

@@ -653,14 +653,14 @@ RAW_DATA = [
def solve_qubo():
"""Solve the Qubo problem."""
"""solve the Qubo problem."""
# Constraint programming engine
# Build the model.
model = cp_model.CpModel()
num_vars = len(RAW_DATA)
all_vars = range(num_vars)
variables = [model.NewBoolVar("x_%i" % i) for i in all_vars]
variables = [model.new_bool_var("x_%i" % i) for i in all_vars]
obj_vars = []
obj_coeffs = []
@@ -672,10 +672,10 @@ def solve_qubo():
if coeff == 0.0:
continue
x_j = variables[j]
var = model.NewBoolVar("")
model.AddBoolOr([x_i.Not(), x_j.Not(), var])
model.AddImplication(var, x_i)
model.AddImplication(var, x_j)
var = model.new_bool_var("")
model.add_bool_or([x_i.negated(), x_j.negated(), var])
model.add_implication(var, x_i)
model.add_implication(var, x_j)
obj_vars.append(var)
obj_coeffs.append(coeff)
@@ -685,14 +685,14 @@ def solve_qubo():
obj_vars.append(variables[i])
obj_coeffs.append(self_coeff)
model.Minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
model.minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
### Solve model.
solver = cp_model.CpSolver()
solver.parameters.num_search_workers = 16
solver.parameters.log_search_progress = True
solver.parameters.max_time_in_seconds = 30
solver.Solve(model)
solver.solve(model)
def main(argv: Sequence[str]) -> None:

186
examples/python/rcpsp_sat.py Executable file → Normal file
View File

@@ -19,10 +19,10 @@ Introduction to the problem:
Data use in flags:
http://www.om-db.wi.tum.de/psplib/data.html
"""
import collections
from typing import Optional
from absl import app
from absl import flags
@@ -46,7 +46,7 @@ _HORIZON = flags.DEFINE_integer("horizon", -1, "Force horizon.")
_ADD_REDUNDANT_ENERGETIC_CONSTRAINTS = flags.DEFINE_bool(
"add_redundant_energetic_constraints",
False,
"Add redundant energetic constraints on the pairs of tasks extracted from"
"add redundant energetic constraints on the pairs of tasks extracted from"
+ " precedence graph.",
)
_DELAY_TIME_LIMIT = flags.DEFINE_float(
@@ -63,7 +63,7 @@ _PREEMPTIVE_LB_TIME_LIMIT = flags.DEFINE_float(
)
def PrintProblemStatistics(problem):
def print_problem_statistics(problem: rcpsp_pb2.RcpspProblem):
"""Display various statistics on the problem."""
# Determine problem type.
@@ -108,7 +108,9 @@ def PrintProblemStatistics(problem):
print(f" - {tasks_with_delay} tasks with successor delays")
def AnalyseDependencyGraph(problem):
def analyse_dependency_graph(
problem: rcpsp_pb2.RcpspProblem,
) -> tuple[list[tuple[int, int, list[int]]], dict[int, list[int]]]:
"""Analyses the dependency graph to improve the model.
Args:
@@ -144,7 +146,7 @@ def AnalyseDependencyGraph(problem):
# Search for pair of tasks, containing at least two parallel branch between
# them in the precedence graph.
num_candidates = 0
result = []
result: list[tuple[int, int, list[int]]] = []
for source, start_outs in outs.items():
if len(start_outs) <= 1:
# Starting with the unique successor of source will be as good.
@@ -177,27 +179,27 @@ def AnalyseDependencyGraph(problem):
result.append((source, sink, common))
# Sort entries lexicographically by (len(common), source, sink)
def Price(entry):
def price(entry):
return num_nodes * num_nodes * len(entry[2]) + num_nodes * entry[0] + entry[1]
result.sort(key=Price)
result.sort(key=price)
print(f" - created {len(result)} pairs of nodes to examine", flush=True)
return result, after
def SolveRcpsp(
problem,
proto_file,
params,
active_tasks,
source,
sink,
intervals_of_tasks,
delays,
in_main_solve=False,
initial_solution=None,
lower_bound=0,
):
def solve_rcpsp(
problem: rcpsp_pb2.RcpspProblem,
proto_file: str,
params: str,
active_tasks: set[int],
source: int,
sink: int,
intervals_of_tasks: list[tuple[int, int, list[int]]],
delays: dict[tuple[int, int], tuple[int, int]],
in_main_solve: bool = False,
initial_solution: Optional[rcpsp_pb2.RcpspAssignment] = None,
lower_bound: int = 0,
) -> tuple[int, int, Optional[rcpsp_pb2.RcpspAssignment]]:
"""Parse and solve a given RCPSP problem in proto format.
The model will only look at the tasks {source} + {sink} + active_tasks, and
@@ -224,7 +226,7 @@ def SolveRcpsp(
"""
# Create the model.
model = cp_model.CpModel()
model.SetName(problem.name)
model.name = problem.name
num_resources = len(problem.resources)
@@ -269,16 +271,16 @@ def SolveRcpsp(
num_recipes = len(task.recipes)
all_recipes = range(num_recipes)
start_var = model.NewIntVar(0, horizon, f"start_of_task_{t}")
end_var = model.NewIntVar(0, horizon, f"end_of_task_{t}")
start_var = model.new_int_var(0, horizon, f"start_of_task_{t}")
end_var = model.new_int_var(0, horizon, f"end_of_task_{t}")
literals = []
if num_recipes > 1:
# Create one literal per recipe.
literals = [model.NewBoolVar(f"is_present_{t}_{r}") for r in all_recipes]
literals = [model.new_bool_var(f"is_present_{t}_{r}") for r in all_recipes]
# Exactly one recipe must be performed.
model.AddExactlyOne(literals)
model.add_exactly_one(literals)
else:
literals = [1]
@@ -293,19 +295,19 @@ def SolveRcpsp(
demand_matrix[(resource, recipe_index)] = demand
# Create the duration variable from the accumulated durations.
duration_var = model.NewIntVarFromDomain(
cp_model.Domain.FromValues(task_to_recipe_durations[t]),
duration_var = model.new_int_var_from_domain(
cp_model.Domain.from_values(task_to_recipe_durations[t]),
f"duration_of_task_{t}",
)
# Link the recipe literals and the duration_var.
for r in range(num_recipes):
model.Add(duration_var == task_to_recipe_durations[t][r]).OnlyEnforceIf(
model.add(duration_var == task_to_recipe_durations[t][r]).only_enforce_if(
literals[r]
)
# Create the interval of the task.
task_interval = model.NewIntervalVar(
task_interval = model.new_interval_var(
start_var, duration_var, end_var, f"task_interval_{t}"
)
@@ -320,14 +322,14 @@ def SolveRcpsp(
for res in all_resources:
demands = [demand_matrix[(res, recipe)] for recipe in all_recipes]
task_resource_to_fixed_demands[(t, res)] = demands
demand_var = model.NewIntVarFromDomain(
cp_model.Domain.FromValues(demands), f"demand_{t}_{res}"
demand_var = model.new_int_var_from_domain(
cp_model.Domain.from_values(demands), f"demand_{t}_{res}"
)
task_to_resource_demands[t].append(demand_var)
# Link the recipe literals and the demand_var.
for r in all_recipes:
model.Add(demand_var == demand_matrix[(res, r)]).OnlyEnforceIf(
model.add(demand_var == demand_matrix[(res, r)]).only_enforce_if(
literals[r]
)
@@ -348,10 +350,13 @@ def SolveRcpsp(
)
# Create makespan variable
makespan = model.NewIntVar(lower_bound, horizon, "makespan")
makespan_size = model.NewIntVar(1, horizon, "interval_makespan_size")
interval_makespan = model.NewIntervalVar(
makespan, makespan_size, model.NewConstant(horizon + 1), "interval_makespan"
makespan = model.new_int_var(lower_bound, horizon, "makespan")
makespan_size = model.new_int_var(1, horizon, "interval_makespan_size")
interval_makespan = model.new_interval_var(
makespan,
makespan_size,
model.new_constant(horizon + 1),
"interval_makespan",
)
# Add precedences.
@@ -370,21 +375,21 @@ def SolveRcpsp(
p1 = task_to_presence_literals[task_id][m1]
if next_id == sink:
delay = delay_matrix.recipe_delays[m1].min_delays[0]
model.Add(s1 + delay <= makespan).OnlyEnforceIf(p1)
model.add(s1 + delay <= makespan).only_enforce_if(p1)
else:
for m2 in range(num_next_modes):
delay = delay_matrix.recipe_delays[m1].min_delays[m2]
s2 = task_starts[next_id]
p2 = task_to_presence_literals[next_id][m2]
model.Add(s1 + delay <= s2).OnlyEnforceIf([p1, p2])
model.add(s1 + delay <= s2).only_enforce_if([p1, p2])
else:
# Normal dependencies (task ends before the start of successors).
for t in all_active_tasks:
for n in problem.tasks[t].successors:
if n == sink:
model.Add(task_ends[t] <= makespan)
model.add(task_ends[t] <= makespan)
elif n in active_tasks:
model.Add(task_ends[t] <= task_starts[n])
model.add(task_ends[t] <= task_starts[n])
# Containers for resource investment problems.
capacities = [] # Capacity variables for all resources.
@@ -404,8 +409,8 @@ def SolveRcpsp(
demands = [task_to_resource_demands[t][res] for t in all_active_tasks]
if problem.is_resource_investment:
capacity = model.NewIntVar(0, c, f"capacity_of_{res}")
model.AddCumulative(intervals, demands, capacity)
capacity = model.new_int_var(0, c, f"capacity_of_{res}")
model.add_cumulative(intervals, demands, capacity)
capacities.append(capacity)
max_cost += c * resource.unit_cost
else: # Standard renewable resource.
@@ -413,7 +418,7 @@ def SolveRcpsp(
intervals.append(interval_makespan)
demands.append(c)
model.AddCumulative(intervals, demands, c)
model.add_cumulative(intervals, demands, c)
else: # Non empty non renewable resource. (single mode only)
if problem.is_consumer_producer:
reservoir_starts = []
@@ -424,15 +429,15 @@ def SolveRcpsp(
reservoir_demands.append(
task_resource_to_fixed_demands[(t, res)][0]
)
model.AddReservoirConstraint(
model.add_reservoir_constraint(
reservoir_starts,
reservoir_demands,
resource.min_capacity,
resource.max_capacity,
)
else: # No producer-consumer. We just sum the demands.
model.Add(
cp_model.LinearExpr.Sum(
model.add(
cp_model.LinearExpr.sum(
[task_to_resource_demands[t][res] for t in all_active_tasks]
)
<= c
@@ -440,8 +445,8 @@ def SolveRcpsp(
# Objective.
if problem.is_resource_investment:
objective = model.NewIntVar(0, max_cost, "capacity_costs")
model.Add(
objective = model.new_int_var(0, max_cost, "capacity_costs")
model.add(
objective
== sum(
problem.resources[i].unit_cost * capacities[i]
@@ -451,17 +456,17 @@ def SolveRcpsp(
else:
objective = makespan
model.Minimize(objective)
model.minimize(objective)
# Add min delay constraints.
if delays is not None:
for (local_start, local_end), (min_delay, _) in delays.items():
if local_start == source and local_end in active_tasks:
model.Add(task_starts[local_end] >= min_delay)
model.add(task_starts[local_end] >= min_delay)
elif local_start in active_tasks and local_end == sink:
model.Add(makespan >= task_ends[local_start] + min_delay)
model.add(makespan >= task_ends[local_start] + min_delay)
elif local_start in active_tasks and local_end in active_tasks:
model.Add(task_starts[local_end] >= task_ends[local_start] + min_delay)
model.add(task_starts[local_end] >= task_ends[local_start] + min_delay)
problem_is_single_mode = True
for t in all_active_tasks:
@@ -504,7 +509,7 @@ def SolveRcpsp(
if sum_of_max_energies <= c * min_delay:
ignored_constraits += 1
continue
model.Add(
model.add(
c * (task_starts[local_end] - task_ends[local_start])
>= sum(task_resource_to_energy[(t, res)] for t in common)
)
@@ -518,15 +523,15 @@ def SolveRcpsp(
# Add solution hint.
if initial_solution:
for t in all_active_tasks:
model.AddHint(task_starts[t], initial_solution.start_of_task[t])
model.add_hint(task_starts[t], initial_solution.start_of_task[t])
if len(task_to_presence_literals[t]) > 1:
selected = initial_solution.selected_recipe_of_task[t]
model.AddHint(task_to_presence_literals[t][selected], 1)
model.add_hint(task_to_presence_literals[t][selected], 1)
# Write model to file.
if proto_file:
print(f"Writing proto to{proto_file}")
model.ExportToFile(proto_file)
model.export_to_file(proto_file)
# Solve model.
solver = cp_model.CpSolver()
@@ -548,28 +553,35 @@ def SolveRcpsp(
if in_main_solve:
solver.parameters.log_search_progress = True
#
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
assignment = rcpsp_pb2.RcpspAssignment()
for t, _ in enumerate(problem.tasks):
if t in task_starts:
assignment.start_of_task.append(solver.Value(task_starts[t]))
assignment.start_of_task.append(solver.value(task_starts[t]))
for r, recipe_literal in enumerate(task_to_presence_literals[t]):
if solver.BooleanValue(recipe_literal):
if solver.boolean_value(recipe_literal):
assignment.selected_recipe_of_task.append(r)
break
else: # t is not an active task.
assignment.start_of_task.append(0)
assignment.selected_recipe_of_task.append(0)
return (
int(solver.BestObjectiveBound()),
int(solver.ObjectiveValue()),
int(solver.best_objective_bound),
int(solver.objective_value),
assignment,
)
return -1, -1, None
def ComputeDelaysBetweenNodes(problem, task_intervals):
def compute_delays_between_nodes(
problem: rcpsp_pb2.RcpspProblem,
task_intervals: list[tuple[int, int, list[int]]],
) -> tuple[
dict[tuple[int, int], tuple[int, int]],
Optional[rcpsp_pb2.RcpspAssignment],
bool,
]:
"""Computes the min delays between all pairs of tasks in 'task_intervals'.
Args:
@@ -594,11 +606,11 @@ def ComputeDelaysBetweenNodes(problem, task_intervals):
num_delays_not_found = 0
optimal_found = True
for start_task, end_task, active_tasks in task_intervals:
min_delay, feasible_delay, assignment = SolveRcpsp(
min_delay, feasible_delay, assignment = solve_rcpsp(
problem,
"",
f"num_search_workers:16,max_time_in_seconds:{_DELAY_TIME_LIMIT.value}",
active_tasks,
set(active_tasks),
start_task,
end_task,
[],
@@ -623,7 +635,13 @@ def ComputeDelaysBetweenNodes(problem, task_intervals):
return delays, complete_problem_assignment, optimal_found
def AcceptNewCandidate(problem, after, demand_map, current, candidate):
def accept_new_candidate(
problem: rcpsp_pb2.RcpspProblem,
after: dict[int, list[int]],
demand_map: dict[tuple[int, int], int],
current: list[int],
candidate: int,
) -> bool:
"""Check if candidate is compatible with the tasks in current."""
for c in current:
if candidate in after[c] or c in after[candidate]:
@@ -643,7 +661,11 @@ def AcceptNewCandidate(problem, after, demand_map, current, candidate):
return True
def ComputePreemptiveLowerBound(problem, after, lower_bound):
def compute_preemptive_lower_bound(
problem: rcpsp_pb2.RcpspProblem,
after: dict[int, list[int]],
lower_bound: int,
) -> int:
"""Computes a preemtive lower bound for the makespan statically.
For this, it breaks all intervals into a set of intervals of size one.
@@ -696,7 +718,7 @@ def ComputePreemptiveLowerBound(problem, after, lower_bound):
new_combinations = [[t]]
for c in all_combinations:
if AcceptNewCandidate(problem, after, demand_map, c, t):
if accept_new_candidate(problem, after, demand_map, c, t):
new_combinations.append(c + [t])
all_combinations.extend(new_combinations)
@@ -705,14 +727,14 @@ def ComputePreemptiveLowerBound(problem, after, lower_bound):
if len(all_combinations) > 5000000:
return lower_bound # Abort if too large.
# Solve the selection model.
# solve the selection model.
# TODO(user): a few possible improvements:
# 1/ use "dominating" columns, i.e. if you can add a task to a column, then
# do not use that column.
# 2/ Merge all task with exactly same demands into one.
model = cp_model.CpModel()
model.SetName(f"lower_bound_{problem.name}")
model.name = f"lower_bound_{problem.name}"
vars_per_task = collections.defaultdict(list)
all_vars = []
@@ -720,29 +742,29 @@ def ComputePreemptiveLowerBound(problem, after, lower_bound):
min_duration = max_duration
for t in c:
min_duration = min(min_duration, duration_map[t])
count = model.NewIntVar(0, min_duration, f"count_{c}")
count = model.new_int_var(0, min_duration, f"count_{c}")
all_vars.append(count)
for t in c:
vars_per_task[t].append(count)
# Each task must be performed.
for t in all_active_tasks:
model.Add(sum(vars_per_task[t]) >= duration_map[t])
model.add(sum(vars_per_task[t]) >= duration_map[t])
# Objective
objective_var = model.NewIntVar(lower_bound, sum_of_demands, "objective_var")
model.Add(objective_var == sum(all_vars))
objective_var = model.new_int_var(lower_bound, sum_of_demands, "objective_var")
model.add(objective_var == sum(all_vars))
model.Minimize(objective_var)
model.minimize(objective_var)
# Solve model.
# solve model.
solver = cp_model.CpSolver()
solver.parameters.num_search_workers = 16
solver.parameters.max_time_in_seconds = _PREEMPTIVE_LB_TIME_LIMIT.value
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
status_str = "optimal" if status == cp_model.OPTIMAL else ""
lower_bound = max(lower_bound, int(solver.BestObjectiveBound()))
lower_bound = max(lower_bound, int(solver.best_objective_bound))
print(f" - {status_str} static lower bound = {lower_bound}", flush=True)
return lower_bound
@@ -753,10 +775,10 @@ def main(_):
rcpsp_parser.parse_file(_INPUT.value)
problem = rcpsp_parser.problem()
PrintProblemStatistics(problem)
print_problem_statistics(problem)
intervals_of_tasks, after = AnalyseDependencyGraph(problem)
delays, initial_solution, optimal_found = ComputeDelaysBetweenNodes(
intervals_of_tasks, after = analyse_dependency_graph(problem)
delays, initial_solution, optimal_found = compute_delays_between_nodes(
problem, intervals_of_tasks
)
@@ -764,9 +786,9 @@ def main(_):
key = (0, last_task)
lower_bound = delays[key][0] if key in delays else 0
if not optimal_found and _PREEMPTIVE_LB_TIME_LIMIT.value > 0.0:
lower_bound = ComputePreemptiveLowerBound(problem, after, lower_bound)
lower_bound = compute_preemptive_lower_bound(problem, after, lower_bound)
SolveRcpsp(
solve_rcpsp(
problem=problem,
proto_file=_OUTPUT_PROTO.value,
params=_PARAMS.value,

130
examples/python/shift_scheduling_sat.py
View File

@@ -17,8 +17,8 @@
from absl import app
from absl import flags
from ortools.sat.python import cp_model
from google.protobuf import text_format
from ortools.sat.python import cp_model
_OUTPUT_PROTO = flags.DEFINE_string(
"output_proto", "", "Output file to write the cp_model proto to."
@@ -28,7 +28,9 @@ _PARAMS = flags.DEFINE_string(
)
def negated_bounded_span(works, start, length):
def negated_bounded_span(
works: list[cp_model.BoolVarT], start: int, length: int
) -> list[cp_model.BoolVarT]:
"""Filters an isolated sub-sequence of variables assined to True.
Extract the span of Boolean variables [start, start + length), negate them,
@@ -46,20 +48,28 @@ def negated_bounded_span(works, start, length):
or by the start or end of works.
"""
sequence = []
# Left border (start of works, or works[start - 1])
# left border (start of works, or works[start - 1])
if start > 0:
sequence.append(works[start - 1])
for i in range(length):
sequence.append(works[start + i].Not())
# Right border (end of works or works[start + length])
sequence.append(works[start + i].negated())
# right border (end of works or works[start + length])
if start + length < len(works):
sequence.append(works[start + length])
return sequence
def add_soft_sequence_constraint(
model, works, hard_min, soft_min, min_cost, soft_max, hard_max, max_cost, prefix
):
model: cp_model.CpModel,
works: list[cp_model.BoolVarT],
hard_min: int,
soft_min: int,
min_cost: int,
soft_max: int,
hard_max: int,
max_cost: int,
prefix: str,
) -> tuple[list[cp_model.BoolVarT], list[int]]:
"""Sequence constraint on true variables with soft and hard bounds.
This constraint look at every maximal contiguous sequence of variables
@@ -93,7 +103,7 @@ def add_soft_sequence_constraint(
# Forbid sequences that are too short.
for length in range(1, hard_min):
for start in range(len(works) - length + 1):
model.AddBoolOr(negated_bounded_span(works, start, length))
model.add_bool_or(negated_bounded_span(works, start, length))
# Penalize sequences that are below the soft limit.
if min_cost > 0:
@@ -101,9 +111,9 @@ def add_soft_sequence_constraint(
for start in range(len(works) - length + 1):
span = negated_bounded_span(works, start, length)
name = ": under_span(start=%i, length=%i)" % (start, length)
lit = model.NewBoolVar(prefix + name)
lit = model.new_bool_var(prefix + name)
span.append(lit)
model.AddBoolOr(span)
model.add_bool_or(span)
cost_literals.append(lit)
# We filter exactly the sequence with a short length.
# The penalty is proportional to the delta with soft_min.
@@ -115,23 +125,33 @@ def add_soft_sequence_constraint(
for start in range(len(works) - length + 1):
span = negated_bounded_span(works, start, length)
name = ": over_span(start=%i, length=%i)" % (start, length)
lit = model.NewBoolVar(prefix + name)
lit = model.new_bool_var(prefix + name)
span.append(lit)
model.AddBoolOr(span)
model.add_bool_or(span)
cost_literals.append(lit)
# Cost paid is max_cost * excess length.
cost_coefficients.append(max_cost * (length - soft_max))
# Just forbid any sequence of true variables with length hard_max + 1
for start in range(len(works) - hard_max):
model.AddBoolOr([works[i].Not() for i in range(start, start + hard_max + 1)])
model.add_bool_or(
[works[i].negated() for i in range(start, start + hard_max + 1)]
)
return cost_literals, cost_coefficients
def add_soft_sum_constraint(
model, works, hard_min, soft_min, min_cost, soft_max, hard_max, max_cost, prefix
):
"""Sum constraint with soft and hard bounds.
model: cp_model.CpModel,
works: list[cp_model.BoolVarT],
hard_min: int,
soft_min: int,
min_cost: int,
soft_max: int,
hard_max: int,
max_cost: int,
prefix: str,
) -> tuple[list[cp_model.IntVar], list[int]]:
"""sum constraint with soft and hard bounds.
This constraint counts the variables assigned to true from works.
If forbids sum < hard_min or > hard_max.
@@ -160,33 +180,33 @@ def add_soft_sum_constraint(
"""
cost_variables = []
cost_coefficients = []
sum_var = model.NewIntVar(hard_min, hard_max, "")
sum_var = model.new_int_var(hard_min, hard_max, "")
# This adds the hard constraints on the sum.
model.Add(sum_var == sum(works))
model.add(sum_var == sum(works))
# Penalize sums below the soft_min target.
if soft_min > hard_min and min_cost > 0:
delta = model.NewIntVar(-len(works), len(works), "")
model.Add(delta == soft_min - sum_var)
delta = model.new_int_var(-len(works), len(works), "")
model.add(delta == soft_min - sum_var)
# TODO(user): Compare efficiency with only excess >= soft_min - sum_var.
excess = model.NewIntVar(0, 7, prefix + ": under_sum")
model.AddMaxEquality(excess, [delta, 0])
excess = model.new_int_var(0, 7, prefix + ": under_sum")
model.add_max_equality(excess, [delta, 0])
cost_variables.append(excess)
cost_coefficients.append(min_cost)
# Penalize sums above the soft_max target.
if soft_max < hard_max and max_cost > 0:
delta = model.NewIntVar(-7, 7, "")
model.Add(delta == sum_var - soft_max)
excess = model.NewIntVar(0, 7, prefix + ": over_sum")
model.AddMaxEquality(excess, [delta, 0])
delta = model.new_int_var(-7, 7, "")
model.add(delta == sum_var - soft_max)
excess = model.new_int_var(0, 7, prefix + ": over_sum")
model.add_max_equality(excess, [delta, 0])
cost_variables.append(excess)
cost_coefficients.append(max_cost)
return cost_variables, cost_coefficients
def solve_shift_scheduling(params, output_proto):
def solve_shift_scheduling(params: str, output_proto: str):
"""Solves the shift scheduling problem."""
# Data
num_employees = 8
@@ -281,22 +301,22 @@ def solve_shift_scheduling(params, output_proto):
for e in range(num_employees):
for s in range(num_shifts):
for d in range(num_days):
work[e, s, d] = model.NewBoolVar("work%i_%i_%i" % (e, s, d))
work[e, s, d] = model.new_bool_var("work%i_%i_%i" % (e, s, d))
# Linear terms of the objective in a minimization context.
obj_int_vars = []
obj_int_coeffs = []
obj_bool_vars = []
obj_bool_coeffs = []
obj_int_vars: list[cp_model.IntVar] = []
obj_int_coeffs: list[int] = []
obj_bool_vars: list[cp_model.BoolVarT] = []
obj_bool_coeffs: list[int] = []
# Exactly one shift per day.
for e in range(num_employees):
for d in range(num_days):
model.AddExactlyOne(work[e, s, d] for s in range(num_shifts))
model.add_exactly_one(work[e, s, d] for s in range(num_shifts))
# Fixed assignments.
for e, s, d in fixed_assignments:
model.Add(work[e, s, d] == 1)
model.add(work[e, s, d] == 1)
# Employee requests
for e, s, d, w in requests:
@@ -348,17 +368,17 @@ def solve_shift_scheduling(params, output_proto):
for e in range(num_employees):
for d in range(num_days - 1):
transition = [
work[e, previous_shift, d].Not(),
work[e, next_shift, d + 1].Not(),
work[e, previous_shift, d].negated(),
work[e, next_shift, d + 1].negated(),
]
if cost == 0:
model.AddBoolOr(transition)
model.add_bool_or(transition)
else:
trans_var = model.NewBoolVar(
trans_var = model.new_bool_var(
"transition (employee=%i, day=%i)" % (e, d)
)
transition.append(trans_var)
model.AddBoolOr(transition)
model.add_bool_or(transition)
obj_bool_vars.append(trans_var)
obj_bool_coeffs.append(cost)
@@ -369,18 +389,18 @@ def solve_shift_scheduling(params, output_proto):
works = [work[e, s, w * 7 + d] for e in range(num_employees)]
# Ignore Off shift.
min_demand = weekly_cover_demands[d][s - 1]
worked = model.NewIntVar(min_demand, num_employees, "")
model.Add(worked == sum(works))
worked = model.new_int_var(min_demand, num_employees, "")
model.add(worked == sum(works))
over_penalty = excess_cover_penalties[s - 1]
if over_penalty > 0:
name = "excess_demand(shift=%i, week=%i, day=%i)" % (s, w, d)
excess = model.NewIntVar(0, num_employees - min_demand, name)
model.Add(excess == worked - min_demand)
excess = model.new_int_var(0, num_employees - min_demand, name)
model.add(excess == worked - min_demand)
obj_int_vars.append(excess)
obj_int_coeffs.append(over_penalty)
# Objective
model.Minimize(
model.minimize(
sum(obj_bool_vars[i] * obj_bool_coeffs[i] for i in range(len(obj_bool_vars)))
+ sum(obj_int_vars[i] * obj_int_coeffs[i] for i in range(len(obj_int_vars)))
)
@@ -395,7 +415,7 @@ def solve_shift_scheduling(params, output_proto):
if params:
text_format.Parse(params, solver.parameters)
solution_printer = cp_model.ObjectiveSolutionPrinter()
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
# Print solution.
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
@@ -408,32 +428,32 @@ def solve_shift_scheduling(params, output_proto):
schedule = ""
for d in range(num_days):
for s in range(num_shifts):
if solver.BooleanValue(work[e, s, d]):
if solver.boolean_value(work[e, s, d]):
schedule += shifts[s] + " "
print("worker %i: %s" % (e, schedule))
print()
print("Penalties:")
for i, var in enumerate(obj_bool_vars):
if solver.BooleanValue(var):
if solver.boolean_value(var):
penalty = obj_bool_coeffs[i]
if penalty > 0:
print(" %s violated, penalty=%i" % (var.Name(), penalty))
print(f" {var.name} violated, penalty={penalty}")
else:
print(" %s fulfilled, gain=%i" % (var.Name(), -penalty))
print(f" {var.name} fulfilled, gain={-penalty}")
for i, var in enumerate(obj_int_vars):
if solver.Value(var) > 0:
if solver.value(var) > 0:
print(
" %s violated by %i, linear penalty=%i"
% (var.Name(), solver.Value(var), obj_int_coeffs[i])
% (var.name, solver.value(var), obj_int_coeffs[i])
)
print()
print("Statistics")
print(" - status : %s" % solver.StatusName(status))
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - status : %s" % solver.status_name(status))
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
def main(_):

36
examples/python/single_machine_scheduling_with_setup_release_due_dates_sat.py
View File

@@ -48,7 +48,7 @@ class SolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Called after each new solution found."""
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, self.WallTime(), self.ObjectiveValue())
% (self.__solution_count, self.wall_time, self.objective_value)
)
self.__solution_count += 1
@@ -433,34 +433,34 @@ def single_machine_scheduling():
% (job_id, release_date, duration, due_date)
)
name_suffix = "_%i" % job_id
start = model.NewIntVar(release_date, due_date, "s" + name_suffix)
end = model.NewIntVar(release_date, due_date, "e" + name_suffix)
interval = model.NewIntervalVar(start, duration, end, "i" + name_suffix)
start = model.new_int_var(release_date, due_date, "s" + name_suffix)
end = model.new_int_var(release_date, due_date, "e" + name_suffix)
interval = model.new_interval_var(start, duration, end, "i" + name_suffix)
starts.append(start)
ends.append(end)
intervals.append(interval)
# No overlap constraint.
model.AddNoOverlap(intervals)
model.add_no_overlap(intervals)
# ----------------------------------------------------------------------------
# Transition times using a circuit constraint.
arcs = []
for i in all_jobs:
# Initial arc from the dummy node (0) to a task.
start_lit = model.NewBoolVar("")
start_lit = model.new_bool_var("")
arcs.append((0, i + 1, start_lit))
# If this task is the first, set to minimum starting time.
min_start_time = max(release_dates[i], setup_times[0][i])
model.Add(starts[i] == min_start_time).OnlyEnforceIf(start_lit)
model.add(starts[i] == min_start_time).only_enforce_if(start_lit)
# Final arc from an arc to the dummy node.
arcs.append((i + 1, 0, model.NewBoolVar("")))
arcs.append((i + 1, 0, model.new_bool_var("")))
for j in all_jobs:
if i == j:
continue
lit = model.NewBoolVar("%i follows %i" % (j, i))
lit = model.new_bool_var("%i follows %i" % (j, i))
arcs.append((i + 1, j + 1, lit))
# We add the reified precedence to link the literal with the times of the
@@ -468,27 +468,27 @@ def single_machine_scheduling():
# If release_dates[j] == 0, we can strenghten this precedence into an
# equality as we are minimizing the makespan.
if release_dates[j] == 0:
model.Add(starts[j] == ends[i] + setup_times[i + 1][j]).OnlyEnforceIf(
model.add(starts[j] == ends[i] + setup_times[i + 1][j]).only_enforce_if(
lit
)
else:
model.Add(starts[j] >= ends[i] + setup_times[i + 1][j]).OnlyEnforceIf(
model.add(starts[j] >= ends[i] + setup_times[i + 1][j]).only_enforce_if(
lit
)
model.AddCircuit(arcs)
model.add_circuit(arcs)
# ----------------------------------------------------------------------------
# Precedences.
for before, after in precedences:
print("job %i is after job %i" % (after, before))
model.Add(ends[before] <= starts[after])
model.add(ends[before] <= starts[after])
# ----------------------------------------------------------------------------
# Objective.
makespan = model.NewIntVar(0, horizon, "makespan")
model.AddMaxEquality(makespan, ends)
model.Minimize(makespan)
makespan = model.new_int_var(0, horizon, "makespan")
model.add_max_equality(makespan, ends)
model.minimize(makespan)
# ----------------------------------------------------------------------------
# Write problem to file.
@@ -503,11 +503,11 @@ def single_machine_scheduling():
if parameters:
text_format.Parse(parameters, solver.parameters)
solution_printer = SolutionPrinter()
solver.Solve(model, solution_printer)
solver.solve(model, solution_printer)
for job_id in all_jobs:
print(
"job %i starts at %i end ends at %i"
% (job_id, solver.Value(starts[job_id]), solver.Value(ends[job_id]))
% (job_id, solver.value(starts[job_id]), solver.value(ends[job_id]))
)

38
examples/python/spread_robots_sat.py
View File

@@ -12,7 +12,7 @@
# See the License for the specific language governing permissions and
# limitations under the License.
"""Maximize the minimum of pairwise distances between n robots in a square space."""
"""maximize the minimum of pairwise distances between n robots in a square space."""
import math
from typing import Sequence
@@ -38,8 +38,8 @@ def spread_robots(num_robots: int, room_size: int, params: str):
model = cp_model.CpModel()
# Create the list of coordinates (x, y) for each robot.
x = [model.NewIntVar(1, room_size, f"x_{i}") for i in range(num_robots)]
y = [model.NewIntVar(1, room_size, f"y_{i}") for i in range(num_robots)]
x = [model.new_int_var(1, room_size, f"x_{i}") for i in range(num_robots)]
y = [model.new_int_var(1, room_size, f"y_{i}") for i in range(num_robots)]
# The specification of the problem is to maximize the minimum euclidian
# distance between any two robots. Unfortunately, the euclidian distance
@@ -58,7 +58,7 @@ def spread_robots(num_robots: int, room_size: int, params: str):
# forall i:
# scaled_min_square_distance <= scaling * (x_diff_sq[i] + y_diff_sq[i])
scaling = 1000
scaled_min_square_distance = model.NewIntVar(
scaled_min_square_distance = model.new_int_var(
0, 2 * scaling * room_size**2, "scaled_min_square_distance"
)
@@ -67,45 +67,45 @@ def spread_robots(num_robots: int, room_size: int, params: str):
for i in range(num_robots - 1):
for j in range(i + 1, num_robots):
# Compute the distance on each dimension between robot i and robot j.
x_diff = model.NewIntVar(-room_size, room_size, f"x_diff{i}")
y_diff = model.NewIntVar(-room_size, room_size, f"y_diff{i}")
model.Add(x_diff == x[i] - x[j])
model.Add(y_diff == y[i] - y[j])
x_diff = model.new_int_var(-room_size, room_size, f"x_diff{i}")
y_diff = model.new_int_var(-room_size, room_size, f"y_diff{i}")
model.add(x_diff == x[i] - x[j])
model.add(y_diff == y[i] - y[j])
# Compute the square of the previous differences.
x_diff_sq = model.NewIntVar(0, room_size**2, f"x_diff_sq{i}")
y_diff_sq = model.NewIntVar(0, room_size**2, f"y_diff_sq{i}")
model.AddMultiplicationEquality(x_diff_sq, x_diff, x_diff)
model.AddMultiplicationEquality(y_diff_sq, y_diff, y_diff)
x_diff_sq = model.new_int_var(0, room_size**2, f"x_diff_sq{i}")
y_diff_sq = model.new_int_var(0, room_size**2, f"y_diff_sq{i}")
model.add_multiplication_equality(x_diff_sq, x_diff, x_diff)
model.add_multiplication_equality(y_diff_sq, y_diff, y_diff)
# We just need to be <= to the scaled square distance as we are
# maximizing the min distance, which is equivalent as maximizing the min
# square distance.
model.Add(scaled_min_square_distance <= scaling * (x_diff_sq + y_diff_sq))
model.add(scaled_min_square_distance <= scaling * (x_diff_sq + y_diff_sq))
# Naive symmetry breaking.
for i in range(1, num_robots):
model.Add(x[0] <= x[i])
model.Add(y[0] <= y[i])
model.add(x[0] <= x[i])
model.add(y[0] <= y[i])
# Objective
model.Maximize(scaled_min_square_distance)
model.maximize(scaled_min_square_distance)
# Creates a solver and solves the model.
solver = cp_model.CpSolver()
if params:
text_format.Parse(params, solver.parameters)
solver.parameters.log_search_progress = True
status = solver.Solve(model)
status = solver.solve(model)
# Prints the solution.
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
print(
f"Spread {num_robots} with a min pairwise distance of"
f" {math.sqrt(solver.ObjectiveValue() / scaling)}"
f" {math.sqrt(solver.objective_value / scaling)}"
)
for i in range(num_robots):
print(f"robot {i}: x={solver.Value(x[i])} y={solver.Value(y[i])}")
print(f"robot {i}: x={solver.value(x[i])} y={solver.value(y[i])}")
else:
print("No solution found.")

100
examples/python/steel_mill_slab_sat.py Executable file → Normal file
View File

@@ -131,22 +131,22 @@ class SteelMillSlabSolutionPrinter(cp_model.CpSolverSolutionCallback):
def on_solution_callback(self):
"""Called on each new solution."""
current_time = time.time()
objective = sum(self.Value(l) for l in self.__loss)
objective = sum(self.value(l) for l in self.__loss)
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, current_time - self.__start_time, objective)
)
self.__solution_count += 1
orders_in_slab = [
[o for o in self.__all_orders if self.Value(self.__assign[o][s])]
[o for o in self.__all_orders if self.value(self.__assign[o][s])]
for s in self.__all_slabs
]
for s in self.__all_slabs:
if orders_in_slab[s]:
line = " - slab %i, load = %i, loss = %i, orders = [" % (
s,
self.Value(self.__load[s]),
self.Value(self.__loss[s]),
self.value(self.__load[s]),
self.value(self.__loss[s]),
)
for o in orders_in_slab[s]:
line += "#%i(w%i, c%i) " % (
@@ -193,44 +193,48 @@ def steel_mill_slab(problem, break_symmetries):
# Create the model and the decision variables.
model = cp_model.CpModel()
assign = [
[model.NewBoolVar("assign_%i_to_slab_%i" % (o, s)) for s in all_slabs]
[model.new_bool_var("assign_%i_to_slab_%i" % (o, s)) for s in all_slabs]
for o in all_orders
]
loads = [model.NewIntVar(0, max_capacity, "load_of_slab_%i" % s) for s in all_slabs]
loads = [
model.new_int_var(0, max_capacity, "load_of_slab_%i" % s) for s in all_slabs
]
color_is_in_slab = [
[model.NewBoolVar("color_%i_in_slab_%i" % (c + 1, s)) for c in all_colors]
[model.new_bool_var("color_%i_in_slab_%i" % (c + 1, s)) for c in all_colors]
for s in all_slabs
]
# Compute load of all slabs.
for s in all_slabs:
model.Add(sum(assign[o][s] * widths[o] for o in all_orders) == loads[s])
model.add(sum(assign[o][s] * widths[o] for o in all_orders) == loads[s])
# Orders are assigned to one slab.
for o in all_orders:
model.AddExactlyOne(assign[o])
model.add_exactly_one(assign[o])
# Redundant constraint (sum of loads == sum of widths).
model.Add(sum(loads) == sum(widths))
model.add(sum(loads) == sum(widths))
# Link present_colors and assign.
for c in all_colors:
for s in all_slabs:
for o in orders_per_color[c]:
model.AddImplication(assign[o][s], color_is_in_slab[s][c])
model.AddImplication(color_is_in_slab[s][c].Not(), assign[o][s].Not())
model.add_implication(assign[o][s], color_is_in_slab[s][c])
model.add_implication(
color_is_in_slab[s][c].negated(), assign[o][s].negated()
)
# At most two colors per slab.
for s in all_slabs:
model.Add(sum(color_is_in_slab[s]) <= 2)
model.add(sum(color_is_in_slab[s]) <= 2)
# Project previous constraint on unique_color_orders
for s in all_slabs:
model.Add(sum(assign[o][s] for o in unique_color_orders) <= 2)
model.add(sum(assign[o][s] for o in unique_color_orders) <= 2)
# Symmetry breaking.
for s in range(num_slabs - 1):
model.Add(loads[s] >= loads[s + 1])
model.add(loads[s] >= loads[s + 1])
# Collect equivalent orders.
width_to_unique_color_order = {}
@@ -271,38 +275,38 @@ def steel_mill_slab(problem, break_symmetries):
positions = {}
for p in ordered_equivalent_orders:
if p[0] not in positions:
positions[p[0]] = model.NewIntVar(
positions[p[0]] = model.new_int_var(
0, num_slabs - 1, "position_of_slab_%i" % p[0]
)
model.AddMapDomain(positions[p[0]], assign[p[0]])
model.add_map_domain(positions[p[0]], assign[p[0]])
if p[1] not in positions:
positions[p[1]] = model.NewIntVar(
positions[p[1]] = model.new_int_var(
0, num_slabs - 1, "position_of_slab_%i" % p[1]
)
model.AddMapDomain(positions[p[1]], assign[p[1]])
model.add_map_domain(positions[p[1]], assign[p[1]])
# Finally add the symmetry breaking constraint.
model.Add(positions[p[0]] <= positions[p[1]])
model.add(positions[p[0]] <= positions[p[1]])
# Objective.
obj = model.NewIntVar(0, num_slabs * max_loss, "obj")
losses = [model.NewIntVar(0, max_loss, "loss_%i" % s) for s in all_slabs]
obj = model.new_int_var(0, num_slabs * max_loss, "obj")
losses = [model.new_int_var(0, max_loss, "loss_%i" % s) for s in all_slabs]
for s in all_slabs:
model.AddElement(loads[s], loss_array, losses[s])
model.Add(obj == sum(losses))
model.Minimize(obj)
model.add_element(loads[s], loss_array, losses[s])
model.add(obj == sum(losses))
model.minimize(obj)
### Solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
objective_printer = cp_model.ObjectiveSolutionPrinter()
status = solver.Solve(model, objective_printer)
status = solver.solve(model, objective_printer)
### Output the solution.
if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
print(
"Loss = %i, time = %f s, %i conflicts"
% (solver.ObjectiveValue(), solver.WallTime(), solver.NumConflicts())
% (solver.objective_value, solver.wall_time, solver.num_conflicts)
)
else:
print("No solution")
@@ -381,11 +385,11 @@ def steel_mill_slab_with_valid_slabs(problem, break_symmetries):
# Create the model and the decision variables.
model = cp_model.CpModel()
assign = [
[model.NewBoolVar("assign_%i_to_slab_%i" % (o, s)) for s in all_slabs]
[model.new_bool_var("assign_%i_to_slab_%i" % (o, s)) for s in all_slabs]
for o in all_orders
]
loads = [model.NewIntVar(0, max_capacity, "load_%i" % s) for s in all_slabs]
losses = [model.NewIntVar(0, max_loss, "loss_%i" % s) for s in all_slabs]
loads = [model.new_int_var(0, max_capacity, "load_%i" % s) for s in all_slabs]
losses = [model.new_int_var(0, max_loss, "loss_%i" % s) for s in all_slabs]
unsorted_valid_slabs = collect_valid_slabs_dp(
capacities, colors, widths, loss_array
@@ -394,20 +398,20 @@ def steel_mill_slab_with_valid_slabs(problem, break_symmetries):
valid_slabs = sorted(unsorted_valid_slabs, key=lambda c: 1000 * c[-1] + c[-2])
for s in all_slabs:
model.AddAllowedAssignments(
model.add_allowed_assignments(
[assign[o][s] for o in all_orders] + [losses[s], loads[s]], valid_slabs
)
# Orders are assigned to one slab.
for o in all_orders:
model.AddExactlyOne(assign[o])
model.add_exactly_one(assign[o])
# Redundant constraint (sum of loads == sum of widths).
model.Add(sum(loads) == sum(widths))
model.add(sum(loads) == sum(widths))
# Symmetry breaking.
for s in range(num_slabs - 1):
model.Add(loads[s] >= loads[s + 1])
model.add(loads[s] >= loads[s + 1])
# Collect equivalent orders.
if break_symmetries:
@@ -453,20 +457,20 @@ def steel_mill_slab_with_valid_slabs(problem, break_symmetries):
positions = {}
for p in ordered_equivalent_orders:
if p[0] not in positions:
positions[p[0]] = model.NewIntVar(
positions[p[0]] = model.new_int_var(
0, num_slabs - 1, "position_of_slab_%i" % p[0]
)
model.AddMapDomain(positions[p[0]], assign[p[0]])
model.add_map_domain(positions[p[0]], assign[p[0]])
if p[1] not in positions:
positions[p[1]] = model.NewIntVar(
positions[p[1]] = model.new_int_var(
0, num_slabs - 1, "position_of_slab_%i" % p[1]
)
model.AddMapDomain(positions[p[1]], assign[p[1]])
model.add_map_domain(positions[p[1]], assign[p[1]])
# Finally add the symmetry breaking constraint.
model.Add(positions[p[0]] <= positions[p[1]])
model.add(positions[p[0]] <= positions[p[1]])
# Objective.
model.Minimize(sum(losses))
model.minimize(sum(losses))
print("Model created")
@@ -476,13 +480,13 @@ def steel_mill_slab_with_valid_slabs(problem, break_symmetries):
text_format.Parse(_PARAMS.value, solver.parameters)
solution_printer = SteelMillSlabSolutionPrinter(orders, assign, loads, losses)
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
### Output the solution.
if status == cp_model.OPTIMAL:
print(
"Loss = %i, time = %.2f s, %i conflicts"
% (solver.ObjectiveValue(), solver.WallTime(), solver.NumConflicts())
% (solver.objective_value, solver.wall_time, solver.num_conflicts)
)
else:
print("No solution")
@@ -522,21 +526,21 @@ def steel_mill_slab_with_column_generation(problem):
# create model and decision variables.
model = cp_model.CpModel()
selected = [model.NewBoolVar("selected_%i" % i) for i in all_valid_slabs]
selected = [model.new_bool_var("selected_%i" % i) for i in all_valid_slabs]
for order_id in all_orders:
model.Add(
model.add(
sum(selected[i] for i, slab in enumerate(valid_slabs) if slab[order_id])
== 1
)
# Redundant constraint (sum of loads == sum of widths).
model.Add(
model.add(
sum(selected[i] * valid_slabs[i][-1] for i in all_valid_slabs) == sum(widths)
)
# Objective.
model.Minimize(sum(selected[i] * valid_slabs[i][-2] for i in all_valid_slabs))
model.minimize(sum(selected[i] * valid_slabs[i][-2] for i in all_valid_slabs))
print("Model created")
@@ -545,13 +549,13 @@ def steel_mill_slab_with_column_generation(problem):
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
solution_printer = cp_model.ObjectiveSolutionPrinter()
status = solver.Solve(model, solution_printer)
status = solver.solve(model, solution_printer)
### Output the solution.
if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
print(
"Loss = %i, time = %.2f s, %i conflicts"
% (solver.ObjectiveValue(), solver.WallTime(), solver.NumConflicts())
% (solver.objective_value, solver.wall_time, solver.num_conflicts)
)
else:
print("No solution")

16
examples/python/sudoku_sat.py Normal file → Executable file
View File

@@ -42,15 +42,15 @@ def solve_sudoku():
grid = {}
for i in line:
for j in line:
grid[(i, j)] = model.NewIntVar(1, line_size, "grid %i %i" % (i, j))
grid[(i, j)] = model.new_int_var(1, line_size, "grid %i %i" % (i, j))
# AllDifferent on rows.
for i in line:
model.AddAllDifferent(grid[(i, j)] for j in line)
model.add_all_different(grid[(i, j)] for j in line)
# AllDifferent on columns.
for j in line:
model.AddAllDifferent(grid[(i, j)] for i in line)
model.add_all_different(grid[(i, j)] for i in line)
# AllDifferent on cells.
for i in cell:
@@ -60,20 +60,20 @@ def solve_sudoku():
for dj in cell:
one_cell.append(grid[(i * cell_size + di, j * cell_size + dj)])
model.AddAllDifferent(one_cell)
model.add_all_different(one_cell)
# Initial values.
for i in line:
for j in line:
if initial_grid[i][j]:
model.Add(grid[(i, j)] == initial_grid[i][j])
model.add(grid[(i, j)] == initial_grid[i][j])
# Solve and print out the solution.
# Solves and prints out the solution.
solver = cp_model.CpSolver()
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL:
for i in line:
print([int(solver.Value(grid[(i, j)])) for j in line])
print([int(solver.value(grid[(i, j)])) for j in line])
solve_sudoku()

34
examples/python/task_allocation_sat.py
View File

@@ -246,12 +246,12 @@ def task_allocation_sat():
assign = {}
for task in all_tasks:
for slot in all_slots:
assign[(task, slot)] = model.NewBoolVar("x[%i][%i]" % (task, slot))
count = model.NewIntVar(0, nslots, "count")
slot_used = [model.NewBoolVar("slot_used[%i]" % s) for s in all_slots]
assign[(task, slot)] = model.new_bool_var("x[%i][%i]" % (task, slot))
count = model.new_int_var(0, nslots, "count")
slot_used = [model.new_bool_var("slot_used[%i]" % s) for s in all_slots]
for task in all_tasks:
model.Add(
model.add(
sum(
assign[(task, slot)] for slot in all_slots if available[task][slot] == 1
)
@@ -259,38 +259,40 @@ def task_allocation_sat():
)
for slot in all_slots:
model.Add(
model.add(
sum(
assign[(task, slot)] for task in all_tasks if available[task][slot] == 1
)
<= capacity
)
model.AddBoolOr(
model.add_bool_or(
[assign[(task, slot)] for task in all_tasks if available[task][slot] == 1]
).OnlyEnforceIf(slot_used[slot])
).only_enforce_if(slot_used[slot])
for task in all_tasks:
if available[task][slot] == 1:
model.AddImplication(slot_used[slot].Not(), assign[(task, slot)].Not())
model.add_implication(
slot_used[slot].negated(), assign[(task, slot)].negated()
)
else:
model.Add(assign[(task, slot)] == 0)
model.add(assign[(task, slot)] == 0)
model.Add(count == sum(slot_used))
model.add(count == sum(slot_used))
# Redundant constraint. This instance is easier if we add this constraint.
# model.Add(count >= (nslots + capacity - 1) // capacity)
# model.add(count >= (nslots + capacity - 1) // capacity)
model.Minimize(count)
model.minimize(count)
# Create a solver and solve the problem.
solver = cp_model.CpSolver()
# Uses the portfolion of heuristics.
solver.parameters.log_search_progress = True
solver.parameters.num_search_workers = 16
status = solver.Solve(model)
status = solver.solve(model)
print("Statistics")
print(" - status =", solver.StatusName(status))
print(" - optimal solution =", solver.ObjectiveValue())
print(" - wall time : %f s" % solver.WallTime())
print(" - status =", solver.status_name(status))
print(" - optimal solution =", solver.objective_value)
print(" - wall time : %f s" % solver.wall_time)
def main(argv: Sequence[str]) -> None:

46
examples/python/tasks_and_workers_assignment_sat.py
View File

@@ -29,13 +29,13 @@ class ObjectivePrinter(cp_model.CpSolverSolutionCallback):
def on_solution_callback(self):
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, self.WallTime(), self.ObjectiveValue())
% (self.__solution_count, self.wall_time, self.objective_value)
)
self.__solution_count += 1
def tasks_and_workers_assignment_sat():
"""Solve the assignment problem."""
"""solve the assignment problem."""
model = cp_model.CpModel()
# CP-SAT solver is integer only.
@@ -53,71 +53,71 @@ def tasks_and_workers_assignment_sat():
x = {}
for i in all_workers:
for j in all_groups:
x[i, j] = model.NewBoolVar("x[%i,%i]" % (i, j))
x[i, j] = model.new_bool_var("x[%i,%i]" % (i, j))
## y_kj is 1 if task k is assigned to group j
y = {}
for k in all_tasks:
for j in all_groups:
y[k, j] = model.NewBoolVar("x[%i,%i]" % (k, j))
y[k, j] = model.new_bool_var("x[%i,%i]" % (k, j))
# Constraints
# Each task k is assigned to a group and only one.
for k in all_tasks:
model.Add(sum(y[k, j] for j in all_groups) == 1)
model.add(sum(y[k, j] for j in all_groups) == 1)
# Each worker i is assigned to a group and only one.
for i in all_workers:
model.Add(sum(x[i, j] for j in all_groups) == 1)
model.add(sum(x[i, j] for j in all_groups) == 1)
# cost per group
# Cost per group
sum_of_costs = sum(task_cost)
averages = []
num_workers_in_group = []
scaled_sum_of_costs_in_group = []
scaling = 1000 # We introduce scaling to deal with floating point average.
for j in all_groups:
n = model.NewIntVar(1, num_workers, "num_workers_in_group_%i" % j)
model.Add(n == sum(x[i, j] for i in all_workers))
c = model.NewIntVar(0, sum_of_costs * scaling, "sum_of_costs_of_group_%i" % j)
model.Add(c == sum(y[k, j] * task_cost[k] * scaling for k in all_tasks))
a = model.NewIntVar(0, sum_of_costs * scaling, "average_cost_of_group_%i" % j)
model.AddDivisionEquality(a, c, n)
n = model.new_int_var(1, num_workers, "num_workers_in_group_%i" % j)
model.add(n == sum(x[i, j] for i in all_workers))
c = model.new_int_var(0, sum_of_costs * scaling, "sum_of_costs_of_group_%i" % j)
model.add(c == sum(y[k, j] * task_cost[k] * scaling for k in all_tasks))
a = model.new_int_var(0, sum_of_costs * scaling, "average_cost_of_group_%i" % j)
model.add_division_equality(a, c, n)
averages.append(a)
num_workers_in_group.append(n)
scaled_sum_of_costs_in_group.append(c)
# All workers are assigned.
model.Add(sum(num_workers_in_group) == num_workers)
model.add(sum(num_workers_in_group) == num_workers)
# Objective.
obj = model.NewIntVar(0, sum_of_costs * scaling, "obj")
model.AddMaxEquality(obj, averages)
model.Minimize(obj)
obj = model.new_int_var(0, sum_of_costs * scaling, "obj")
model.add_max_equality(obj, averages)
model.minimize(obj)
# Solve and print out the solution.
solver = cp_model.CpSolver()
solver.parameters.max_time_in_seconds = 60 * 60 * 2
objective_printer = ObjectivePrinter()
status = solver.Solve(model, objective_printer)
print(solver.ResponseStats())
status = solver.solve(model, objective_printer)
print(solver.response_stats())
if status == cp_model.OPTIMAL:
for j in all_groups:
print("Group %i" % j)
for i in all_workers:
if solver.BooleanValue(x[i, j]):
if solver.boolean_value(x[i, j]):
print(" - worker %i" % i)
for k in all_tasks:
if solver.BooleanValue(y[k, j]):
if solver.boolean_value(y[k, j]):
print(" - task %i with cost %i" % (k, task_cost[k]))
print(
" - sum_of_costs = %i"
% (solver.Value(scaled_sum_of_costs_in_group[j]) // scaling)
% (solver.value(scaled_sum_of_costs_in_group[j]) // scaling)
)
print(" - average cost = %f" % (solver.Value(averages[j]) * 1.0 / scaling))
print(" - average cost = %f" % (solver.value(averages[j]) * 1.0 / scaling))
tasks_and_workers_assignment_sat()

12
examples/python/tsp_sat.py
View File

@@ -82,17 +82,17 @@ def main():
if i == j:
continue
lit = model.NewBoolVar("%i follows %i" % (j, i))
lit = model.new_bool_var("%i follows %i" % (j, i))
arcs.append((i, j, lit))
arc_literals[i, j] = lit
obj_vars.append(lit)
obj_coeffs.append(DISTANCE_MATRIX[i][j])
model.AddCircuit(arcs)
model.add_circuit(arcs)
# Minimize weighted sum of arcs. Because this s
model.Minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
model.minimize(sum(obj_vars[i] * obj_coeffs[i] for i in range(len(obj_vars))))
# Solve and print out the solution.
solver = cp_model.CpSolver()
@@ -100,8 +100,8 @@ def main():
# To benefit from the linearization of the circuit constraint.
solver.parameters.linearization_level = 2
solver.Solve(model)
print(solver.ResponseStats())
solver.solve(model)
print(solver.response_stats())
current_node = 0
str_route = "%i" % current_node
@@ -111,7 +111,7 @@ def main():
for i in all_nodes:
if i == current_node:
continue
if solver.BooleanValue(arc_literals[current_node, i]):
if solver.boolean_value(arc_literals[current_node, i]):
str_route += " -> %i" % i
route_distance += DISTANCE_MATRIX[current_node][i]
current_node = i

34
examples/python/vendor_scheduling_sat.py
View File

@@ -48,13 +48,13 @@ class SolutionPrinter(cp_model.CpSolverSolutionCallback):
for i in range(self.__num_vendors):
print(
" - vendor %i: " % i,
self.__possible_schedules[self.Value(self.__selected_schedules[i])],
self.__possible_schedules[self.value(self.__selected_schedules[i])],
)
print()
for j in range(self.__num_hours):
print(" - # workers on day%2i: " % j, end=" ")
print(self.Value(self.__hours_stat[j]), end=" ")
print(self.value(self.__hours_stat[j]), end=" ")
print()
print()
@@ -101,38 +101,40 @@ def vendor_scheduling_sat():
all_hours = range(num_hours)
#
# declare variables
# Declare variables
#
x = {}
for v in all_vendors:
tmp = []
for h in all_hours:
x[v, h] = model.NewIntVar(0, num_work_types, "x[%i,%i]" % (v, h))
x[v, h] = model.new_int_var(0, num_work_types, "x[%i,%i]" % (v, h))
tmp.append(x[v, h])
selected_schedule = model.NewIntVar(0, num_possible_schedules - 1, "s[%i]" % v)
hours = model.NewIntVar(0, num_hours, "h[%i]" % v)
selected_schedule = model.new_int_var(
0, num_possible_schedules - 1, "s[%i]" % v
)
hours = model.new_int_var(0, num_hours, "h[%i]" % v)
selected_schedules.append(selected_schedule)
vendors_stat.append(hours)
tmp.append(selected_schedule)
tmp.append(hours)
model.AddAllowedAssignments(tmp, possible_schedules)
model.add_allowed_assignments(tmp, possible_schedules)
#
# Statistics and constraints for each hour
#
for h in all_hours:
workers = model.NewIntVar(0, 1000, "workers[%i]" % h)
model.Add(workers == sum(x[v, h] for v in all_vendors))
workers = model.new_int_var(0, 1000, "workers[%i]" % h)
model.add(workers == sum(x[v, h] for v in all_vendors))
hours_stat.append(workers)
model.Add(workers * max_traffic_per_vendor >= traffic[h])
model.add(workers * max_traffic_per_vendor >= traffic[h])
#
# Redundant constraint: sort selected_schedules
#
for v in range(num_vendors - 1):
model.Add(selected_schedules[v] <= selected_schedules[v + 1])
model.add(selected_schedules[v] <= selected_schedules[v + 1])
# Solve model.
solver = cp_model.CpSolver()
@@ -145,13 +147,13 @@ def vendor_scheduling_sat():
hours_stat,
min_vendors,
)
status = solver.Solve(model, solution_printer)
print("Status = %s" % solver.StatusName(status))
status = solver.solve(model, solution_printer)
print("Status = %s" % solver.status_name(status))
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
print(" - number of solutions found: %i" % solution_printer.solution_count())

42
examples/python/wedding_optimal_chart_sat.py
View File

@@ -56,7 +56,7 @@ class WeddingChartPrinter(cp_model.CpSolverSolutionCallback):
def on_solution_callback(self):
current_time = time.time()
objective = self.ObjectiveValue()
objective = self.objective_value
print(
"Solution %i, time = %f s, objective = %i"
% (self.__solution_count, current_time - self.__start_time, objective)
@@ -66,10 +66,10 @@ class WeddingChartPrinter(cp_model.CpSolverSolutionCallback):
for t in range(self.__num_tables):
print("Table %d: " % t)
for g in range(self.__num_guests):
if self.Value(self.__seats[(t, g)]):
if self.value(self.__seats[(t, g)]):
print(" " + self.__names[g])
def num_solutions(self):
def num_solutions(self) -> int:
return self.__solution_count
@@ -148,12 +148,12 @@ def solve_with_discrete_model():
seats = {}
for t in all_tables:
for g in all_guests:
seats[(t, g)] = model.NewBoolVar("guest %i seats on table %i" % (g, t))
seats[(t, g)] = model.new_bool_var("guest %i seats on table %i" % (g, t))
colocated = {}
for g1 in range(num_guests - 1):
for g2 in range(g1 + 1, num_guests):
colocated[(g1, g2)] = model.NewBoolVar(
colocated[(g1, g2)] = model.new_bool_var(
"guest %i seats with guest %i" % (g1, g2)
)
@@ -161,12 +161,12 @@ def solve_with_discrete_model():
for g1 in range(num_guests - 1):
for g2 in range(g1 + 1, num_guests):
for t in all_tables:
same_table[(g1, g2, t)] = model.NewBoolVar(
same_table[(g1, g2, t)] = model.new_bool_var(
"guest %i seats with guest %i on table %i" % (g1, g2, t)
)
# Objective
model.Maximize(
model.maximize(
sum(
connections[g1][g2] * colocated[g1, g2]
for g1 in range(num_guests - 1)
@@ -181,35 +181,35 @@ def solve_with_discrete_model():
# Everybody seats at one table.
for g in all_guests:
model.Add(sum(seats[(t, g)] for t in all_tables) == 1)
model.add(sum(seats[(t, g)] for t in all_tables) == 1)
# Tables have a max capacity.
for t in all_tables:
model.Add(sum(seats[(t, g)] for g in all_guests) <= table_capacity)
model.add(sum(seats[(t, g)] for g in all_guests) <= table_capacity)
# Link colocated with seats
for g1 in range(num_guests - 1):
for g2 in range(g1 + 1, num_guests):
for t in all_tables:
# Link same_table and seats.
model.AddBoolOr(
model.add_bool_or(
[
seats[(t, g1)].Not(),
seats[(t, g2)].Not(),
seats[(t, g1)].negated(),
seats[(t, g2)].negated(),
same_table[(g1, g2, t)],
]
)
model.AddImplication(same_table[(g1, g2, t)], seats[(t, g1)])
model.AddImplication(same_table[(g1, g2, t)], seats[(t, g2)])
model.add_implication(same_table[(g1, g2, t)], seats[(t, g1)])
model.add_implication(same_table[(g1, g2, t)], seats[(t, g2)])
# Link colocated and same_table.
model.Add(
model.add(
sum(same_table[(g1, g2, t)] for t in all_tables) == colocated[(g1, g2)]
)
# Min known neighbors rule.
for g in all_guests:
model.Add(
model.add(
sum(
same_table[(g, g2, t)]
for g2 in range(g + 1, num_guests)
@@ -226,17 +226,17 @@ def solve_with_discrete_model():
)
# Symmetry breaking. First guest seats on the first table.
model.Add(seats[(0, 0)] == 1)
model.add(seats[(0, 0)] == 1)
### Solve model.
solver = cp_model.CpSolver()
solution_printer = WeddingChartPrinter(seats, names, num_tables, num_guests)
solver.Solve(model, solution_printer)
solver.solve(model, solution_printer)
print("Statistics")
print(" - conflicts : %i" % solver.NumConflicts())
print(" - branches : %i" % solver.NumBranches())
print(" - wall time : %f s" % solver.WallTime())
print(" - conflicts : %i" % solver.num_conflicts)
print(" - branches : %i" % solver.num_branches)
print(" - wall time : %f s" % solver.wall_time)
print(" - num solutions: %i" % solution_printer.num_solutions())

24
examples/python/weighted_latency_problem_sat.py
View File

@@ -12,7 +12,7 @@
# See the License for the specific language governing permissions and
# limitations under the License.
"""Solve a random Weighted Latency problem with the CP-SAT solver."""
"""solve a random Weighted Latency problem with the CP-SAT solver."""
import random
from typing import Sequence
@@ -61,10 +61,12 @@ def solve_with_cp_sat(x, y, profits):
# because of the manhattan distance, the sum of distances is bounded by this.
horizon = _GRID_SIZE.value * 2 * _NUM_NODES.value
times = [model.NewIntVar(0, horizon, f"x_{i}") for i in range(_NUM_NODES.value + 1)]
times = [
model.new_int_var(0, horizon, f"x_{i}") for i in range(_NUM_NODES.value + 1)
]
# Node 0 is the start node.
model.Add(times[0] == 0)
model.add(times[0] == 0)
# Create the circuit constraint.
arcs = []
@@ -74,29 +76,29 @@ def solve_with_cp_sat(x, y, profits):
continue
# We use a manhattan distance between nodes.
distance = abs(x[i] - x[j]) + abs(y[i] - y[j])
lit = model.NewBoolVar(f"{i}_to_{j}")
lit = model.new_bool_var(f"{i}_to_{j}")
arcs.append((i, j, lit))
# Add transitions between nodes.
# add transitions between nodes.
if i == 0:
# Initial transition
model.Add(times[j] == distance).OnlyEnforceIf(lit)
model.add(times[j] == distance).only_enforce_if(lit)
elif j != 0:
# We do not care for the last transition.
model.Add(times[j] == times[i] + distance).OnlyEnforceIf(lit)
model.AddCircuit(arcs)
model.add(times[j] == times[i] + distance).only_enforce_if(lit)
model.add_circuit(arcs)
model.Minimize(cp_model.LinearExpr.WeightedSum(times, profits))
model.minimize(cp_model.LinearExpr.weighted_sum(times, profits))
if _PROTO_FILE.value:
model.ExportToFile(_PROTO_FILE.value)
model.export_to_file(_PROTO_FILE.value)
# Solve model.
solver = cp_model.CpSolver()
if _PARAMS.value:
text_format.Parse(_PARAMS.value, solver.parameters)
solver.parameters.log_search_progress = True
solver.Solve(model)
solver.solve(model)
def main(argv: Sequence[str]) -> None:

110
examples/python/zebra_sat.py Normal file → Executable file
View File

@@ -44,77 +44,77 @@ def solve_zebra():
# Create the model.
model = cp_model.CpModel()
red = model.NewIntVar(1, 5, "red")
green = model.NewIntVar(1, 5, "green")
yellow = model.NewIntVar(1, 5, "yellow")
blue = model.NewIntVar(1, 5, "blue")
ivory = model.NewIntVar(1, 5, "ivory")
red = model.new_int_var(1, 5, "red")
green = model.new_int_var(1, 5, "green")
yellow = model.new_int_var(1, 5, "yellow")
blue = model.new_int_var(1, 5, "blue")
ivory = model.new_int_var(1, 5, "ivory")
englishman = model.NewIntVar(1, 5, "englishman")
spaniard = model.NewIntVar(1, 5, "spaniard")
japanese = model.NewIntVar(1, 5, "japanese")
ukrainian = model.NewIntVar(1, 5, "ukrainian")
norwegian = model.NewIntVar(1, 5, "norwegian")
englishman = model.new_int_var(1, 5, "englishman")
spaniard = model.new_int_var(1, 5, "spaniard")
japanese = model.new_int_var(1, 5, "japanese")
ukrainian = model.new_int_var(1, 5, "ukrainian")
norwegian = model.new_int_var(1, 5, "norwegian")
dog = model.NewIntVar(1, 5, "dog")
snails = model.NewIntVar(1, 5, "snails")
fox = model.NewIntVar(1, 5, "fox")
zebra = model.NewIntVar(1, 5, "zebra")
horse = model.NewIntVar(1, 5, "horse")
dog = model.new_int_var(1, 5, "dog")
snails = model.new_int_var(1, 5, "snails")
fox = model.new_int_var(1, 5, "fox")
zebra = model.new_int_var(1, 5, "zebra")
horse = model.new_int_var(1, 5, "horse")
tea = model.NewIntVar(1, 5, "tea")
coffee = model.NewIntVar(1, 5, "coffee")
water = model.NewIntVar(1, 5, "water")
milk = model.NewIntVar(1, 5, "milk")
fruit_juice = model.NewIntVar(1, 5, "fruit juice")
tea = model.new_int_var(1, 5, "tea")
coffee = model.new_int_var(1, 5, "coffee")
water = model.new_int_var(1, 5, "water")
milk = model.new_int_var(1, 5, "milk")
fruit_juice = model.new_int_var(1, 5, "fruit juice")
old_gold = model.NewIntVar(1, 5, "old gold")
kools = model.NewIntVar(1, 5, "kools")
chesterfields = model.NewIntVar(1, 5, "chesterfields")
lucky_strike = model.NewIntVar(1, 5, "lucky strike")
parliaments = model.NewIntVar(1, 5, "parliaments")
old_gold = model.new_int_var(1, 5, "old gold")
kools = model.new_int_var(1, 5, "kools")
chesterfields = model.new_int_var(1, 5, "chesterfields")
lucky_strike = model.new_int_var(1, 5, "lucky strike")
parliaments = model.new_int_var(1, 5, "parliaments")
model.AddAllDifferent(red, green, yellow, blue, ivory)
model.AddAllDifferent(englishman, spaniard, japanese, ukrainian, norwegian)
model.AddAllDifferent(dog, snails, fox, zebra, horse)
model.AddAllDifferent(tea, coffee, water, milk, fruit_juice)
model.AddAllDifferent(parliaments, kools, chesterfields, lucky_strike, old_gold)
model.add_all_different(red, green, yellow, blue, ivory)
model.add_all_different(englishman, spaniard, japanese, ukrainian, norwegian)
model.add_all_different(dog, snails, fox, zebra, horse)
model.add_all_different(tea, coffee, water, milk, fruit_juice)
model.add_all_different(parliaments, kools, chesterfields, lucky_strike, old_gold)
model.Add(englishman == red)
model.Add(spaniard == dog)
model.Add(coffee == green)
model.Add(ukrainian == tea)
model.Add(green == ivory + 1)
model.Add(old_gold == snails)
model.Add(kools == yellow)
model.Add(milk == 3)
model.Add(norwegian == 1)
model.add(englishman == red)
model.add(spaniard == dog)
model.add(coffee == green)
model.add(ukrainian == tea)
model.add(green == ivory + 1)
model.add(old_gold == snails)
model.add(kools == yellow)
model.add(milk == 3)
model.add(norwegian == 1)
diff_fox_chesterfields = model.NewIntVar(-4, 4, "diff_fox_chesterfields")
model.Add(diff_fox_chesterfields == fox - chesterfields)
model.AddAbsEquality(1, diff_fox_chesterfields)
diff_fox_chesterfields = model.new_int_var(-4, 4, "diff_fox_chesterfields")
model.add(diff_fox_chesterfields == fox - chesterfields)
model.add_abs_equality(1, diff_fox_chesterfields)
diff_horse_kools = model.NewIntVar(-4, 4, "diff_horse_kools")
model.Add(diff_horse_kools == horse - kools)
model.AddAbsEquality(1, diff_horse_kools)
diff_horse_kools = model.new_int_var(-4, 4, "diff_horse_kools")
model.add(diff_horse_kools == horse - kools)
model.add_abs_equality(1, diff_horse_kools)
model.Add(lucky_strike == fruit_juice)
model.Add(japanese == parliaments)
model.add(lucky_strike == fruit_juice)
model.add(japanese == parliaments)
diff_norwegian_blue = model.NewIntVar(-4, 4, "diff_norwegian_blue")
model.Add(diff_norwegian_blue == norwegian - blue)
model.AddAbsEquality(1, diff_norwegian_blue)
diff_norwegian_blue = model.new_int_var(-4, 4, "diff_norwegian_blue")
model.add(diff_norwegian_blue == norwegian - blue)
model.add_abs_equality(1, diff_norwegian_blue)
# Solve and print out the solution.
solver = cp_model.CpSolver()
status = solver.Solve(model)
status = solver.solve(model)
if status == cp_model.OPTIMAL:
people = [englishman, spaniard, japanese, ukrainian, norwegian]
water_drinker = [p for p in people if solver.Value(p) == solver.Value(water)][0]
zebra_owner = [p for p in people if solver.Value(p) == solver.Value(zebra)][0]
print("The", water_drinker.Name(), "drinks water.")
print("The", zebra_owner.Name(), "owns the zebra.")
water_drinker = [p for p in people if solver.value(p) == solver.value(water)][0]
zebra_owner = [p for p in people if solver.value(p) == solver.value(zebra)][0]
print("The", water_drinker.name, "drinks water.")
print("The", zebra_owner.name, "owns the zebra.")
else:
print("No solutions to the zebra problem, this is unusual!")