Skip to content

Commit 8f97701

Browse files
ThomSergThomSerg
committed
Update solveAll
1 parent e31f136 commit 8f97701

File tree

7 files changed

+75
-46
lines changed

7 files changed

+75
-46
lines changed

‎cpmpy/solvers/cpo.py‎

Lines changed: 39 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@
4343
"""
4444

4545
import shutil
46+
import time
4647
import warnings
4748

4849
from .solver_interface import SolverInterface, SolverStatus, ExitStatus
@@ -230,14 +231,28 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
230231

231232
docp = self.get_docp()
232233
solution_count = 0
233-
while solution_limit is None or solution_count < solution_limit:
234-
cpo_result = self.solve(time_limit=time_limit, **kwargs)
235-
if not cpo_result:
236-
break
234+
start = time.time()
235+
while ((time_limit is None) or (time_limit > 0)) and self.solve(time_limit=time_limit, **kwargs):
236+
237+
# display if needed
238+
if display is not None:
239+
if isinstance(display, Expression):
240+
print(argval(display))
241+
elif isinstance(display, list):
242+
print(argvals(display))
243+
else:
244+
display() # callback
245+
246+
# count and stop
237247
solution_count += 1
248+
if solution_count == solution_limit:
249+
break
250+
238251
if self.has_objective():
239252
# only find all optimal solutions
240253
self.cpo_model.add(self.cpo_model.get_objective_expression().children[0] == self.objective_value_)
254+
255+
# add nogood on the user variables
241256
solvars = []
242257
vals = []
243258
for cpm_var in self.user_vars:
@@ -251,13 +266,26 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
251266
solvars.append(sol_var)
252267
vals.append(cpm_value)
253268
self.cpo_model.add(docp.modeler.forbidden_assignments(solvars, [vals]))
254-
if display is not None:
255-
if isinstance(display, Expression):
256-
print(argval(display))
257-
elif isinstance(display, list):
258-
print(argvals(display))
259-
else:
260-
display() # callback
269+
270+
if time_limit is not None: # update remaining time
271+
time_limit -= self.status().runtime
272+
end = time.time()
273+
274+
# update solver status
275+
self.cpm_status.runtime = end - start
276+
if solution_count:
277+
if solution_count == solution_limit:
278+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
279+
elif self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
280+
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
281+
else:
282+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
283+
# else: <- is implicit since nothing needs to update
284+
# if self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
285+
# self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
286+
# elif self.cpm_status.exitstatus == ExitStatus.UNKNOWN:
287+
# self.cpm_status.exitstatus = ExitStatus.UNKNOWN
288+
261289
return solution_count
262290

263291
def solver_var(self, cpm_var):

‎cpmpy/solvers/exact.py‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -322,7 +322,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
322322
timelim = self._update_time(timelim, start, end) # update remaining time
323323

324324
assert my_status in ["UNSAT","SAT","INCONSISTENT","TIMEOUT"], "Unexpected status code for Exact: " + my_status
325-
if my_status == "UNSAT": # found unsatisfiability
325+
if my_status == "UNSAT": # found unsatisfiability (no more solutions to be found)
326326
self._fillVars() # erases the solution
327327
break
328328
elif my_status == "SAT": # found solution, but not optimality proven
@@ -350,7 +350,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
350350
if solsfound: # found some solutions
351351
if solsfound == solution_limit: # matched solution limit
352352
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
353-
elif my_status == "UNSAT": # found all solutions
353+
elif my_status == "UNSAT": # found all solutions (before limits were reached)
354354
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
355355
else: # timeout
356356
self.cpm_status.exitstatus = ExitStatus.FEASIBLE

‎cpmpy/solvers/gcs.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@ def display_callback(solution_map):
300300
self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
301301
elif num_sols >= 1:
302302
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
303-
else: # maybe unsat, maybe not
303+
else: # maybe unsat, maybe not (maybe a timeout)
304304
self.cpm_status.exitstatus = ExitStatus.UNKNOWN
305305

306306
# clear user vars if no solution found

‎cpmpy/solvers/gurobi.py‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -476,6 +476,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
476476
477477
Returns: number of solutions found
478478
"""
479+
from gurobipy import GRB
479480

480481
if time_limit is not None:
481482
self.grb_model.setParam("TimeLimit", time_limit)
@@ -538,10 +539,13 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
538539

539540
if opt_sol_count:
540541
if opt_sol_count == solution_limit:
541-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
542-
elif self.cpm_status.exitstatus == ExitStatus.OPTIMAL:
543-
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
542+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
544543
else:
545-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
544+
grb_status = self.grb_model.Status
545+
if grb_status == GRB.TIME_LIMIT: # reached time limit
546+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
547+
else: # found all solutions
548+
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
549+
# if unsat or timout with no solution, .solve() will have already set the state accordingly (so nothing to update)
546550

547551
return opt_sol_count

‎cpmpy/solvers/minizinc.py‎

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -301,7 +301,7 @@ def solve(self, time_limit=None, **kwargs):
301301

302302
return has_sol
303303

304-
def _post_solve(self, mzn_result):
304+
def _post_solve(self, mzn_result, solve_all:bool=False):
305305
""" shared by solve() and solveAll() """
306306
import minizinc
307307

@@ -324,7 +324,10 @@ def _post_solve(self, mzn_result):
324324
if mzn_status == minizinc.result.Status.SATISFIED:
325325
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
326326
elif mzn_status == minizinc.result.Status.ALL_SOLUTIONS:
327-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
327+
if solve_all:
328+
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
329+
else:
330+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
328331
elif mzn_status == minizinc.result.Status.OPTIMAL_SOLUTION:
329332
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
330333
elif mzn_status == minizinc.result.Status.UNSATISFIABLE:
@@ -400,24 +403,14 @@ async def _solveAll(self, display=None, time_limit=None, solution_limit=None, **
400403
var._value = None
401404

402405
# status handling
403-
self._post_solve(mzn_result)
406+
self._post_solve(mzn_result, solve_all=True)
404407

405408
if solution_count: # found at least one solution
406409
if solution_count == solution_limit: # matched solution limit
407410
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
408-
elif mzn_result.solution is None: # last iteration didn't find a solution
409-
# below states are from the second-last iteration
410-
if self.cpm_status.exitstatus == ExitStatus.OPTIMAL: # timeout
411-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
412-
elif self.cpm_status.exitstatus == ExitStatus.FEASIBLE: # found all solutions
413-
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
414-
else:
415-
raise()
416-
417-
elif time_limit is None or self.cpm_status.runtime < time_limit: # found all solutions
418-
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
419-
else: # timeout
420-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
411+
# elif mzn_result.solution is None: <- is implicit since nothing needs to update
412+
# last iteration didn't find a solution
413+
# nothing needs to update since _post_solve already set state correctly (state from the second-last iteration)
421414

422415
return solution_count
423416

‎cpmpy/solvers/ortools.py‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,12 @@ def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwa
217217
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
218218
# CSP
219219
else:
220-
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
220+
# for .solveAll(), if all solutions found status is OPTIMAL
221+
if kwargs.get("enumerate_all_solutions", False):
222+
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
223+
# regular .solve()
224+
else:
225+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
221226
elif self.ort_status == ort.INFEASIBLE:
222227
self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
223228
elif self.ort_status == ort.MODEL_INVALID:

‎cpmpy/solvers/pysdd.py‎

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -196,32 +196,31 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
196196
else:
197197
projected_sols = set(sddmodels)
198198

199-
if len(projected_sols) >= 1:
200-
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
199+
if projected_sols:
200+
if projected_sols == solution_limit:
201+
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
202+
else:
203+
# time limit not (yet) supported -> always all solutions found
204+
self.cpm_status.exitstatus = ExitStatus.OPTIMAL
201205
else:
202206
self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
203207

204-
if display is None:
205-
# the desired, fast computation
206-
return len(projected_sols)
207-
208-
else:
208+
# display if needed
209+
if display is not None:
209210
# manually walking over the tree, much slower...
210-
solution_count = 0
211211
for sol in projected_sols:
212-
solution_count += 1
213212
# fill in variable values
214213
for i, cpm_var in enumerate(self.user_vars):
215214
cpm_var._value = sol[i]
216215

217-
# display is not None:
218216
if isinstance(display, Expression):
219217
print(argval(display))
220218
elif isinstance(display, list):
221219
print(argvals(display))
222220
else:
223221
display() # callback
224-
return solution_count
222+
223+
return len(projected_sols)
225224

226225
def solver_var(self, cpm_var):
227226
"""

0 commit comments

Comments
 (0)