C++ Reference: sat_proto_solver

Note: This documentation is automatically generated.

Solve the input MIP model with the SAT solver.

If possible, std::move the request into this function call to avoid a copy.

If you need to change the solver parameters, please use the EncodeSatParametersAsString() function below to set the request's solver_specific_parameters field.

The optional interrupt_solve can be used to interrupt the solve early. It must only be set to true, never reset to false. It is also used internally by the solver that will set it to true for its own internal logic. As a consequence the caller should ignore the stored value and should not use the same atomic for different concurrent calls.

The optional logging_callback will be called when the SAT parameter log_search_progress is set to true. Passing a callback will disable the default logging to INFO. Note though that by default the SAT parameter log_to_stdout is true so even with a callback, the logs will appear on stdout too unless log_to_stdout is set to false. The enable_internal_solver_output in the request will act as the SAT parameter log_search_progress.

The optional solution_callback will be called on each intermediate solution found by the solver. The solver may call solution_callback from multiple threads, but it will ensure that at most one thread executes solution_callback at a time.

Function	Type	Arguments	Comments
EncodeSatParametersAsString	Return type: std::string Arguments: const sat::SatParameters& parameters
SatSolveProto	Return type: absl::StatusOr<MPSolutionResponse> Arguments: MPModelRequest request, std::atomic<bool>* interrupt_solve = nullptr, std::function<void(const std::string&)> logging_callback = nullptr, std::function<void(const MPSolution&)> solution_callback = nullptr