Find many CP-SAT solutions, multi-threaded, under time constraint

[Daniel Angelov]

Hi all,

I want to find as many solutions as possible under some time constraint - e.g. 1 minute. 
I am currently using the CP-SAT solver with (minimal example attached below)

solver = cp_model.CpSolver()    
solver.parameters.max_time_in_seconds = 60

And use a `SearchForAllSolutions` to get a callback where I manage a list within the class where the values of the needed variables are appended. 

status = solver.SearchForAllSolutions(model, solution_aggregator)

I want to parallelize the search, as I am trying to find as large of a number of solutions as possible. I alter the number of workers by: 

solver.parameters.num_search_workers = 10

However, it results in failing a check somewhere within or-tools. If I remove the Search for all solutions and leave just `solver.Solve()`, I can confirm that the multiple threads are used and it returns a single solution.

Error (ortools 7.2):

F0806 10:44:06.209460 15492 cp_model_solver.cc:2102] Check failed: !params.enumerate_all_solutions() Enumerating all solutions in parallel is not supported.
*** Check failure stack trace: ***
Aborted (core dumped)

Error (ortools 7.3):

Check failed: !parameters.enumerate_all_solutions() Enumerating all solutions in parallel is not supported.
*** Check failure stack trace: ***
    @     0x7fe3a86cf100  google::LogMessage::Fail()
    @     0x7fe3a86cf05c  google::LogMessage::SendToLog()
    @     0x7fe3a86ce9c0  google::LogMessage::Flush()
    @     0x7fe3a86d1df6  google::LogMessageFatal::~LogMessageFatal()
    @     0x7fe3a5c5b6f6  operations_research::sat::(anonymous namespace)::SolveCpModelParallel()
    @     0x7fe3a5c61afa  operations_research::sat::SolveCpModel()
    @     0x7fe3a8b567dd  _wrap_SatHelper_SolveWithParametersAndSolutionCallback
    @           0x4bc4aa  PyEval_EvalFrameEx
    @           0x4b9b66  PyEval_EvalCodeEx
    @           0x4c1f56  PyEval_EvalFrameEx
    @           0x4b9b66  PyEval_EvalCodeEx
    @           0x4c1f56  PyEval_EvalFrameEx
    @           0x4b9b66  PyEval_EvalCodeEx
    @           0x4eb69f  (unknown)
    @           0x4e58f2  PyRun_FileExFlags
    @           0x4e41a6  PyRun_SimpleFileExFlags
    @           0x4938ce  Py_Main
    @     0x7fe3ab718830  __libc_start_main
    @           0x493299  _start
    @              (nil)  (unknown)
Aborted (core dumped)

Q: I am wondering why is this check enforced? In python, list append is a thread-safe operation. In other languages, it would be left to the user to make sure that the callback has the necessary mutexes and performs thread-safe operations.

An alternative way to bypass this issue is to start the search of different threads and merge the results/solutions.
Q: What is the correct way to specify a seed for the random number generator used within ortools?  

As far as I can see, the solver.Phrase() and SolutionCollector() are for the old solvers. Is there an equivalent for CP-SAT as to specify only the variables that we are interested in (e.g. ignore temp bool variables used for channelling) and collection of solutions?

Bonus Q: Is there a list of all of the parameters that can be set to the model?

Thanks,
Daniel

Minimal example:

from ortools.sat.python import cp_model

class VarArraySolutionAggregator(cp_model.CpSolverSolutionCallback):
    """Print intermediate solutions."""
    def __init__(self, variables):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__variables = variables
        self.__solution_count = 0
        self.__solutions = []

    def on_solution_callback(self):
        self.__solution_count += 1
        s = tuple([self.Value(v) for v in self.__variables])
        self.__solutions.append(s)
        print(s)
   
    @property
    def solution_count(self):
        return self.__solution_count


    @property
    def solutions(self):
        return self.__solutions


def SearchForAllSolutionsSampleSat():
    """Showcases calling the solver to search for all solutions."""
    # Creates the model.
    model = cp_model.CpModel()

    # Creates the variables.
    num_vals = 3
    x = model.NewIntVar(0, num_vals - 1, 'x')
    y = model.NewIntVar(0, num_vals - 1, 'y')
    z = model.NewIntVar(0, num_vals - 1, 'z')

    # Create the constraints.
    model.Add(x != y)

    # Create a solver and solve.
    solver = cp_model.CpSolver()
    # Works ok
    solver.parameters.num_search_workers = 1
    # Fails
    solver.parameters.num_search_workers = 10
    solver.parameters.max_time_in_seconds = 1.

    solution_aggregator = VarArraySolutionAggregator([x, y, z])
    status = solver.SearchForAllSolutions(model, solution_aggregator)

    print('Status = %s' % solver.StatusName(status))
    print('Number of solutions found: %i in %0.2fs' % (solution_aggregator.solution_count, solver.WallTime()))
    print(len(solution_aggregator.solutions))


SearchForAllSolutionsSampleSat()

[Laurent Perron]

1) The difficulty of enumerating all solutions in parallel is not having duplicate solutions. Thus we intentionally forbid it.

2) You have your solution aggregator, it replaces the solution collector. I would not use random seed. Take important variables, explode all the possible assignments of these tuples, and distribute among threads.

3) Parameters: https://github.com/google/or-tools/blob/stable/ortools/sat/sat_parameters.proto

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

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/27c7b6f9-bf4a-4f7d-9350-2a92dcb41426%40googlegroups.com.

[Daniel Angelov]

1. Wouldn't it be relatively possible to maintain a hash or the solutions a get a check in O(1) for a duplicate? So for the whole solution set, it will incur a penalty of +O(n). Similarly, is the solver state serializable? Alternatively, there can be a flag whether duplicate solutions are acceptable (e.g. `False` by default). 
In my case, I am already filtering for duplicates and am left with approx half of the solutions anyway (of the variables of interest).
2. The way constraints are generated is quite involved. Would solution hinting uniformly spread within the domain be softly similar?
3. Thanks!

To unsubscribe from this group and stop receiving emails from it, send an email to or-tools...@googlegroups.com.

[Laurent Perron]

1) It could, but It is low on our priorities.

2) Yes, you can try it. But eventually, the solver will forget hinting.

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

To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/733f2376-5b0c-443b-ae53-75ad807a4a8f%40googlegroups.com.