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

[CP-SAT] add ~operator for the logical negation in C++ and Python; fix a bug in C#

Browse Source
This commit is contained in:
Laurent Perron
2023-12-15 14:10:44 +01:00
parent 47306a72ca
commit 5b911b1169
44 changed files with 229 additions and 235 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
examples/python/bus_driver_scheduling_sat.py
View File

@@ -1863,14 +1863,10 @@ def bus_driver_scheduling(minimize_drivers: bool, max_num_drivers: int) -> int:
# Node not performed
# - set both driving times to 0
# - add a looping arc on the node
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())
model.add(total_driving[d, s] == 0).only_enforce_if(~performed[d, s])
model.add(no_break_driving[d, s] == 0).only_enforce_if(~performed[d, s])
incoming_literals[s].append(~performed[d, s])
outgoing_literals[s].append(~performed[d, s])
# negated adding to the shared lists, because, globally, each node will
# have one incoming literal, and one outgoing literal.
@@ -1919,17 +1915,15 @@ def bus_driver_scheduling(minimize_drivers: bool, max_num_drivers: int) -> int:
if minimize_drivers:
# Driver is not working.
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())
model.add(start_times[d] == min_start_time).only_enforce_if(~working)
model.add(end_times[d] == min_start_time).only_enforce_if(~working)
model.add(driving_times[d] == 0).only_enforce_if(~working)
working_drivers.append(working)
outgoing_source_literals.append(working.negated())
incoming_sink_literals.append(working.negated())
outgoing_source_literals.append(~working)
incoming_sink_literals.append(~working)
# Conditional working time constraints
model.add(working_times[d] >= min_working_time).only_enforce_if(working)
model.add(working_times[d] == 0).only_enforce_if(working.negated())
model.add(working_times[d] == 0).only_enforce_if(~working)
else:
# Working time constraints
model.add(working_times[d] >= min_working_time)
@@ -1959,9 +1953,7 @@ def bus_driver_scheduling(minimize_drivers: bool, max_num_drivers: int) -> int:
if minimize_drivers:
# Push non working drivers to the end
for d in range(num_drivers - 1):
model.add_implication(
working_drivers[d].negated(), working_drivers[d + 1].negated()
)
model.add_implication(~working_drivers[d], ~working_drivers[d + 1])
# Redundant constraints: sum of driving times = sum of shift driving times
model.add(cp_model.LinearExpr.sum(driving_times) == total_driving_time)

2
examples/python/cover_rectangle_sat.py
View File

@@ -71,7 +71,7 @@ def cover_rectangle(num_squares: int) -> bool:
# Define same to be true iff sizes[i] == sizes[i + 1]
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())
model.add(sizes[i] < sizes[i + 1]).only_enforce_if(~same)
# Tie break with starts.
model.add(x_starts[i] <= x_starts[i + 1]).only_enforce_if(same)

4
examples/python/gate_scheduling_sat.py
View File

@@ -93,14 +93,14 @@ def main(_):
start1,
duration,
end1,
performed_on_m0.negated(),
~performed_on_m0,
"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).only_enforce_if(performed_on_m0)
model.add(start1 == start).only_enforce_if(performed_on_m0.negated())
model.add(start1 == start).only_enforce_if(~performed_on_m0)
# Width constraint (modeled as a cumulative)
model.add_cumulative(intervals, demands, max_width)

10
examples/python/knapsack_2d_sat.py
View File

@@ -133,8 +133,8 @@ def solve_with_duplicate_items(data: pd.Series, max_height: int, max_width: int)
)
# Unused boxes are fixed at (0.0).
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())
model.add(x_starts[i] == 0).only_enforce_if(~is_used[i])
model.add(y_starts[i] == 0).only_enforce_if(~is_used[i])
# Constraints.
@@ -235,8 +235,8 @@ def solve_with_duplicate_optional_items(
)
)
# Unused boxes are fixed at (0.0).
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())
model.add(x_starts[i] == 0).only_enforce_if(~is_used[i])
model.add(y_starts[i] == 0).only_enforce_if(~is_used[i])
# Constraints.
@@ -363,7 +363,7 @@ def solve_with_rotations(data: pd.Series, max_height: int, max_width: int):
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.negated())
is_used.append(~not_selected)
## 2D no overlap.
model.add_no_overlap_2d(x_intervals, y_intervals)

10
examples/python/line_balancing_sat.py
View File

@@ -232,26 +232,26 @@ def solve_boolean_model(model, hint):
for p in all_pods:
model.add_implication(assign[t, p], possible[t, p])
if p > 1:
model.add_implication(assign[t, p], possible[t, p - 1].negated())
model.add_implication(assign[t, p], ~possible[t, p - 1])
# Precedences.
for before, after in precedences:
for p in range(1, num_pods):
model.add_implication(assign[before, p], possible[after, p - 1].negated())
model.add_implication(assign[before, p], ~possible[after, p - 1])
# 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.add_implication(a, active[p])
model.add_bool_or(all_assign_vars + [active[p].negated()])
model.add_bool_or(all_assign_vars + [~active[p]])
# 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.add_implication(active[p - 1].negated(), active[p].negated())
model.add_implication(~active[p - 1], ~active[p])
for t in all_tasks:
model.add_implication(active[p].negated(), possible[t, p - 1])
model.add_implication(~active[p], possible[t, p - 1])
# Objective.
model.minimize(sum(active))

4
examples/python/prize_collecting_tsp_sat.py
View File

@@ -129,7 +129,7 @@ def prize_collecting_tsp():
arcs = []
for i in all_nodes:
is_visited = model.new_bool_var(f"{i} is visited")
arcs.append((i, i, is_visited.negated()))
arcs.append((i, i, ~is_visited))
obj_vars.append(is_visited)
obj_coeffs.append(VISIT_VALUES[i])
@@ -137,7 +137,7 @@ def prize_collecting_tsp():
for j in all_nodes:
if i == j:
used_arcs[i, j] = is_visited.negated()
used_arcs[i, j] = ~is_visited
continue
arc_is_used = model.new_bool_var(f"{j} follows {i}")
arcs.append((i, j, arc_is_used))

4
examples/python/prize_collecting_vrp_sat.py
View File

@@ -144,7 +144,7 @@ def prize_collecting_vrp():
arcs = []
for i in all_nodes:
is_visited = model.new_bool_var(f"{i} is visited")
arcs.append((i, i, is_visited.negated()))
arcs.append((i, i, ~is_visited))
obj_vars.append(is_visited)
obj_coeffs.append(VISIT_VALUES[i])
@@ -152,7 +152,7 @@ def prize_collecting_vrp():
for j in all_nodes:
if i == j:
used_arcs[v][i, j] = is_visited.negated()
used_arcs[v][i, j] = ~is_visited
continue
arc_is_used = model.new_bool_var(f"{j} follows {i}")
arcs.append((i, j, arc_is_used))

8
examples/python/qubo_sat.py
View File

@@ -14,11 +14,11 @@
"""Solves a Qubo program using the CP-SAT solver."""
from typing import Sequence
from typing import List, Sequence
from absl import app
from ortools.sat.python import cp_model
RAW_DATA = [
RAW_DATA: List[List[float]] = [
# fmt:off
[
0, 0, 49.774821, -59.5968886, -46.0773896, 0, -65.166109, 0, 0, 0, 0, 0,
@@ -652,7 +652,7 @@ RAW_DATA = [
]
def solve_qubo():
def solve_qubo() -> None:
"""solve the Qubo problem."""
# Build the model.
@@ -673,7 +673,7 @@ def solve_qubo():
continue
x_j = variables[j]
var = model.new_bool_var("")
model.add_bool_or([x_i.negated(), x_j.negated(), var])
model.add_bool_or([~x_i, ~x_j, var])
model.add_implication(var, x_i)
model.add_implication(var, x_j)
obj_vars.append(var)

10
examples/python/shift_scheduling_sat.py
View File

@@ -52,7 +52,7 @@ def negated_bounded_span(
if start > 0:
sequence.append(works[start - 1])
for i in range(length):
sequence.append(works[start + i].negated())
sequence.append(~works[start + i])
# right border (end of works or works[start + length])
if start + length < len(works):
sequence.append(works[start + length])
@@ -134,9 +134,7 @@ def add_soft_sequence_constraint(
# Just forbid any sequence of true variables with length hard_max + 1
for start in range(len(works) - hard_max):
model.add_bool_or(
[works[i].negated() for i in range(start, start + hard_max + 1)]
)
model.add_bool_or([~works[i] for i in range(start, start + hard_max + 1)])
return cost_literals, cost_coefficients
@@ -368,8 +366,8 @@ def solve_shift_scheduling(params: str, output_proto: str):
for e in range(num_employees):
for d in range(num_days - 1):
transition = [
work[e, previous_shift, d].negated(),
work[e, next_shift, d + 1].negated(),
~work[e, previous_shift, d],
~work[e, next_shift, d + 1],
]
if cost == 0:
model.add_bool_or(transition)

4
examples/python/steel_mill_slab_sat.py
View File

@@ -220,9 +220,7 @@ def steel_mill_slab(problem, break_symmetries):
for s in all_slabs:
for o in orders_per_color[c]:
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()
)
model.add_implication(~color_is_in_slab[s][c], ~assign[o][s])
# At most two colors per slab.
for s in all_slabs:

4
examples/python/task_allocation_sat.py
View File

@@ -270,9 +270,7 @@ def task_allocation_sat():
).only_enforce_if(slot_used[slot])
for task in all_tasks:
if available[task][slot] == 1:
model.add_implication(
slot_used[slot].negated(), assign[(task, slot)].negated()
)
model.add_implication(~slot_used[slot], ~assign[(task, slot)])
else:
model.add(assign[(task, slot)] == 0)

4
examples/python/wedding_optimal_chart_sat.py
View File

@@ -194,8 +194,8 @@ def solve_with_discrete_model():
# Link same_table and seats.
model.add_bool_or(
[
seats[(t, g1)].negated(),
seats[(t, g2)].negated(),
~seats[(t, g1)],
~seats[(t, g2)],
same_table[(g1, g2, t)],
]
)