-
Notifications
You must be signed in to change notification settings - Fork 30
Improve example testing #651
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Changes from 14 commits
772b59e
a7491cf
f5bfff4
6180dc9
f48180b
32a469d
9404043
13a2613
28a7dd2
26d1d45
e4c4599
70b00b9
b5b15ac
0f39b8a
cd9fd80
3fa04a2
1c1411e
da8f291
07becb4
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -55,10 +55,9 @@ def explain_ocus(soft, soft_weights=None, hard=[], solver="ortools", verbose=0) | |
# compute all derivable literals | ||
full_sol = solution_intersection(Model(hard + soft), solver, verbose) | ||
|
||
|
||
# prep soft constraint formulation with a literal for each soft constraint | ||
# (so we can iteratively use an assumption solver on softliterals) | ||
soft_lit = BoolVar(shape=len(soft), name="ind") | ||
soft_lit = boolvar(shape=len(soft), name="ind") | ||
reified_soft = [] | ||
for i,bv in enumerate(soft_lit): | ||
reified_soft += [bv.implies(soft[i])] | ||
|
@@ -196,7 +195,7 @@ def explain_one_step_ocus(hard, soft_lit, cost, remaining_sol_to_explain, solver | |
## ----- SAT solver model ---- | ||
SAT = SolverLookup.lookup(solver)(Model(hard)) | ||
|
||
while(True): | ||
while True: | ||
hittingset_solver.solve() | ||
|
||
# Get hitting set | ||
|
@@ -209,7 +208,7 @@ def explain_one_step_ocus(hard, soft_lit, cost, remaining_sol_to_explain, solver | |
print("\n\t hs =", hs, S) | ||
|
||
# SAT check and computation of model | ||
if not SAT.solve(assumptions=S): | ||
if not SAT.solve(assumptions=list(S)): | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. why is this needed, to wrap S? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In the or-tools interface, the
|
||
if verbose > 1: | ||
print("\n\t ===> OCUS =", S) | ||
|
||
|
@@ -242,7 +241,7 @@ def solution_intersection(model, solver="ortools", verbose=False): | |
assert SAT.solve(), "Propagation of soft constraints only possible if model is SAT." | ||
sat_model = set(bv if bv.value() else ~bv for bv in sat_vars) | ||
|
||
while(SAT.solve()): | ||
while SAT.solve(): | ||
# negate the values of the model | ||
sat_model &= set(bv if bv.value() else ~bv for bv in sat_vars) | ||
blocking_clause = ~all(sat_model) | ||
|
@@ -265,11 +264,10 @@ def cost_func(soft, soft_weights): | |
''' | ||
|
||
def cost_lit(cons): | ||
# return soft weight if constraint is a soft constraint | ||
if len(set({cons}) & set(soft)) > 0: | ||
# return soft weight if the constraint is a soft constraint | ||
if len({cons} & set(soft)) > 0: | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this is odd code... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. indeed, corrected. |
||
return soft_weights[soft.index(cons)] | ||
else: | ||
return 1 | ||
return 1 | ||
|
||
return cost_lit | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -116,20 +116,25 @@ def basketball_schedule(): | |
for d in days[:-2]: | ||
if t != DUKE and t != UNC: | ||
# No team plays in two consecutive dates away against UNC and Duke | ||
model += ~((config[d, t] == UNC) & (where[d,t] == AWAY) & | ||
(config[d+1, t] == DUKE) & (where[d+1,t] == AWAY)) | ||
model += ~((config[d, t] == DUKE) & (where[d,t] == AWAY) & | ||
(config[d+1, t] == UNC) & (where[d+1,t] == AWAY)) | ||
model += ((config[d, t] == UNC) & (where[d, t] == AWAY) & | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. your code change removes the ~, the not... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This change fixes an error with the previous version of the constraints. But it is indeed unintuitive, so I changed it back to the earlier version, while keeping the fix of the error. |
||
(config[d + 1, t] == DUKE) & (where[d + 1, t] == AWAY)).implies(False) | ||
model += ((config[d, t] == DUKE) & (where[d, t] == AWAY) & | ||
(config[d + 1, t] == UNC) & (where[d + 1, t] == AWAY)).implies(False) | ||
for d in days[:-3]: | ||
if t not in [UNC, DUKE, WAKE]: | ||
# No team plays in three consecutive dates against UNC, Duke and Wake (independent of home/away). | ||
model += ~((config[d,t] == UNC) & (config[d+1,t] == DUKE) & (config[d+2] == WAKE)) | ||
model += ~((config[d,t] == UNC) & (config[d+1,t] == WAKE) & (config[d+2] == DUKE)) | ||
model += ~((config[d,t] == DUKE) & (config[d+1,t] == UNC) & (config[d+2] == WAKE)) | ||
model += ~((config[d,t] == DUKE) & (config[d+1,t] == WAKE) & (config[d+2] == UNC)) | ||
model += ~((config[d,t] == WAKE) & (config[d+1,t] == UNC) & (config[d+2] == DUKE)) | ||
model += ~((config[d,t] == WAKE) & (config[d+1,t] == DUKE) & (config[d+2] == UNC)) | ||
|
||
model += ((config[d, t] == UNC) & (config[d + 1, t] == DUKE) & (config[d + 2, t] == WAKE)).implies( | ||
False) | ||
model += ((config[d, t] == UNC) & (config[d + 1, t] == WAKE) & (config[d + 2, t] == DUKE)).implies( | ||
False) | ||
model += ((config[d, t] == DUKE) & (config[d + 1, t] == UNC) & (config[d + 2, t] == WAKE)).implies( | ||
False) | ||
model += ((config[d, t] == DUKE) & (config[d + 1, t] == WAKE) & (config[d + 2, t] == UNC)).implies( | ||
False) | ||
model += ((config[d, t] == WAKE) & (config[d + 1, t] == UNC) & (config[d + 2, t] == DUKE)).implies( | ||
False) | ||
model += ((config[d, t] == WAKE) & (config[d + 1, t] == DUKE) & (config[d + 2, t] == UNC)).implies( | ||
False) | ||
|
||
# 9. Other constraints | ||
# UNC plays its rival Duke in the last date and in date 11 | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -23,39 +23,36 @@ | |
|
||
|
||
def progressive_party(n_boats, n_periods, capacity, crew_size, **kwargs): | ||
|
||
is_host = boolvar(shape=n_boats, name="is_host") | ||
visits = intvar(lb=0, ub=n_boats-1, shape=(n_periods,n_boats), name="visits") | ||
visits = intvar(0, n_boats - 1, shape=(n_periods, n_boats), name="visits") | ||
|
||
model = Model() | ||
|
||
# crews of host boats stay on boat | ||
# Crews of host boats stay on boat | ||
for boat in range(n_boats): | ||
model += (is_host[boat]).implies(all(visits[:,boat] == boat)) | ||
model += (is_host[boat]).implies((visits[:, boat] == boat).all()) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. is there a reason to prefer .all() over cp.all(...)? I prefer a cp.all() upfront... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Agreed and reverted. |
||
|
||
# number of visitors can never exceed capacity of boat | ||
# Number of visitors can never exceed capacity of boat | ||
for slot in range(n_periods): | ||
for boat in range(n_boats): | ||
model += sum((visits[slot] == boat) * crew_size) <= capacity[boat] | ||
model += sum((visits[slot] == boat) * crew_size) + crew_size[boat] * is_host[boat] <= capacity[boat] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. was the previous code wrong? the comment says 'number of visitors', so without the crew...? and why does being the host matters for the crew size? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, the constraint was missing the host boat's crew, which is exactly what is added here. The comment was misleading (I corrected it now) as the original problem description specifies that "The total number of people aboard a boat, including the host crew and guest crews, must not exceed the capacity". |
||
|
||
# guests cannot visit a boat twice | ||
# Guests cannot visit a boat twice | ||
for boat in range(n_boats): | ||
# Alldiff must be decomposed in v0.9.8, see issue #105 on github | ||
model += (~is_host[boat]).implies(all((AllDifferent(visits[:,boat]).decompose()))) | ||
model += (~is_host[boat]).implies(AllDifferent(visits[:, boat])) | ||
|
||
# non-host boats cannot be visited | ||
# Non-host boats cannot be visited | ||
for boat in range(n_boats): | ||
model += (~is_host[boat]).implies(all(visits != boat)) | ||
model += (~is_host[boat]).implies((visits != boat).all()) | ||
|
||
# crews cannot meet more than once | ||
# Crews cannot meet more than once | ||
for c1, c2 in all_pairs(range(n_boats)): | ||
model += sum(visits[:,c1] == visits[:,c2]) <= 1 | ||
model += sum(visits[:, c1] == visits[:, c2]) <= 1 | ||
|
||
# minimize number of hosts needed | ||
# Minimize number of hosts needed | ||
model.minimize(sum(is_host)) | ||
|
||
return model, (visits,is_host) | ||
|
||
return model, (visits, is_host) | ||
|
||
|
||
# Helper functions | ||
|
@@ -79,7 +76,7 @@ def _print_instances(data): | |
# argument parsing | ||
url = "https://raw.githubusercontent.com/CPMpy/cpmpy/csplib/examples/csplib/prob013_progressive_party.json" | ||
parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) | ||
parser.add_argument('-instance', nargs='?', default="csplib_example", help="Name of the problem instance found in file 'filename'") | ||
parser.add_argument('-instance', nargs='?', default="lan01", help="Name of the problem instance found in file 'filename'") | ||
parser.add_argument('-filename', nargs='?', default=url, help="File containing problem instances, can be local file or url") | ||
parser.add_argument('--list-instances', help='List all problem instances', action='store_true') | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm surprised these casts are needed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Without the casts, this error is thrown in the master_model solving (OR-tools):
TypeError: Not a number: False of type <class 'numpy.bool_'>