How to stop SAT search after a first (n-th) solution found?

[Motorrat]

Running https://github.com/google/or-tools/blob/master/examples/python/school_scheduling_sat.py seems to go on indefinitely printing "Found Solution!". Is there a way to specify that the search should stop after finding the first (or n first) solution(s)? I see that there is an issue open since 2015 on stopping the process with the Ctrl+C - i.e. that also doesn't help. https://github.com/google/or-tools/issues/18 SAT solver method called in the example is explicitly called SearchForAllSolutions https://github.com/google/or-tools/blob/6961e303a8a1ff2595bc095e598f4c153ff52bfd/ortools/sat/python/cp_model.py#L1114 so ...

[Mizux]

For routing model you can use different SearchLimits options https://developers.google.com/optimization/routing/tsp/routing_options#search-limits

which seems to bind Solver::MakeLimit...

so something like routing.solver.SolutionsLimit(42) ?

EDIT: SWIG Python seems to bind in pywrapcp.py:

class Solver (_object):
[...]
    def TimeLimit(self, time_in_ms: 'int64') -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_TimeLimit(self, time_in_ms)

    def BranchesLimit(self, branches: 'int64') -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_BranchesLimit(self, branches)

    def FailuresLimit(self, failures: 'int64') -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_FailuresLimit(self, failures)

    def SolutionsLimit(self, solutions: 'int64') -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_SolutionsLimit(self, solutions)
        return _pywrapcp.Solver_SolutionsLimit(self, solutions)

    def Limit(self, *args) -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_Limit(self, *args)

    def CustomLimit(self, limiter: 'std::function< bool () >') -> "operations_research::SearchLimit *":
        return _pywrapcp.Solver_CustomLimit(self, limiter)

ps: grep --color -rIin "limit" ~/.local/lib/python3.5/site-packages/ortools/constraint_solver/pywrapcp.py

[Motorrat]

@Mizux While I see how this could be useful aren't SAT and Routing two different codebases? What I found though is the comment from @lperron removing time limit https://github.com/google/or-tools/commit/4cd6ecccb3a6a9f645db5ce0a3770513a8b0cb20#diff-59a2a7bc3737a3a9a3fa9f4448e4ed32

-        const SatSolver::Status status = solver->SolveWithTimeLimit(time_limit);
+        const SatSolver::Status status = solver->Solve();

https://github.com/google/or-tools/blob/master/ortools/sat/cp_model_solver.h#L47

[Motorrat]

Also to give context - my actual problem is that the search in the example https://github.com/google/or-tools/blob/master/examples/python/school_scheduling_sat.py doesn't seem to stop after some tens of minutes elapsed. A helpful example but hard to build on specifically because it is not clear if the search will ever stop.

[Mizux]

Yes you're right, SAT solver also only use/provide a "protobuf message" API that's why method has been removed, contrary to CP which provides both way.

[lperron]

You are right.

We will look at how to add this API on the python API.

Thanks Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le lun. 16 avr. 2018 à 15:25, Mizux notifications@github.com a écrit :

Yes you're right, SAT solver also only use/provide a "protobuf message" API that's why method has been removed, contrary to CP which provides both way.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/651#issuecomment-381597844, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17dc3w0Kb4zVTMeUVR65EZbtu26EJks5tpJuzgaJpZM4TWKGw .

[Motorrat]

It seems like SolveWithSolutionObserver https://github.com/google/or-tools/blob/master/ortools/sat/python/cp_model.py#L1107 is the one I was looking for for this example. it could be just substituted for SearchForAllSolutions https://github.com/google/or-tools/blob/master/examples/python/school_scheduling_sat.py#L123 Could you please confirm?

[lperron]

Both are nearly equivalent. But they do not give you a way to abort the search as model, callbacks and solver are very disconnected.

I hope to have a solution in place before next release (early may??).

--Laurent Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le lun. 16 avr. 2018 à 16:20, Diego Kobylkin notifications@github.com a écrit :

It seems like SolveWithSolutionObserver https://github.com/google/or-tools/blob/master/ortools/sat/python/cp_model.py#L1107 is the one I was looking for for this example. it could be just substituted for SearchForAllSolutions https://github.com/google/or-tools/blob/master/examples/python/school_scheduling_sat.py#L123 Could you please confirm?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/651#issuecomment-381614654, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17b34o9KRdf_vtJ5gt0K3TcYK3bBlks5tpKjCgaJpZM4TWKGw .

[lperron]

Code is submitted and documented:

https://github.com/google/or-tools/blob/master/ortools/sat/doc/solver.md#stopping-search-early

It should be available in v6.9

Closing the issue now.

Thanks