Module Sat.Response

A response from CP-SAT for a given problem.

type status =
  1. | Unknown
    (*

    The solver has not run for long enough.

    *)
  2. | ModelInvalid
    (*

    There is a problem with the model.

    *)
  3. | Feasible
    (*

    The model has a solution but it may not be optimal with respect to the objective.

    *)
  4. | Infeasible
    (*

    The model has no solutions, i.e., the constraints are too restrictive.

    *)
  5. | Optimal
    (*

    The model has a solution and it is optimal with respect to the objective.

    *)

The overall result.

val string_of_status : status -> string

String representing the status.

type vardom = {
  1. name : string;
  2. domain : (int64 * int64) list;
}

The name and restricted domain of a variable.

type objective = {
  1. terms : (int * Var.t_int) list;
  2. offset : float;
  3. scaling_factor : float;
  4. domain : (int64 * int64) list;
  5. scaling_was_exact : bool;
  6. integer_before_offset : int64;
  7. integer_after_offset : int64;
  8. integer_scaling_factor : int64;
}

Information on the objective.

type t = {
  1. status : status;
    (*

    The status of the solve.

    *)
  2. solution : int array;
    (*

    A feasible solution, mapping each variable (index) to an integer value.

    *)
  3. objective_value : float;
    (*

    The value of the objective for the given solution.

    *)
  4. best_objective_bound : float;
    (*

    A proven lower or upper bound on the objective to, respectively, minimize or maximize.

    *)
  5. additional_solutions : int array list;
    (*

    Other solutions if the fill_additional_solutions_in_response parameters is set.

    *)
  6. tightened_variables : vardom list;
    (*

    Reduced variable domains if the fill_tightened_domains_in_response parameter is set.

    *)
  7. sufficient_assumptions_for_infeasibility : Var.t_bool list;
    (*

    A subset of the assumptions field that makes the model infeasible.

    *)
  8. integer_objective : objective option;
    (*

    Integer objective optimized internally.

    *)
  9. integer_objective_lower_bound : int;
    (*

    A lower bound on the integer expression of the objective.

    *)
  10. num_integers : int;
  11. num_booleans : int;
  12. num_fixed_booleans : int;
  13. num_conflicts : int;
  14. num_branches : int;
  15. num_binary_propagations : int;
  16. num_integer_propagations : int;
  17. num_restarts : int;
  18. num_lp_iterations : int;
  19. wall_time : float;
    (*

    Counted from the beginning of the solve call.

    *)
  20. user_time : float;
    (*

    Counted from the beginning of the solve call.

    *)
  21. deterministic_time : float;
    (*

    Counted from the beginning of the solve call.

    *)
  22. gap_integral : float;
    (*

    The integral of log(1 + absolute_objective_gap) over time.

    *)
  23. solution_info : string;
    (*

    Additional information about how the solution was found.

    *)
  24. solve_log : string;
    (*

    Filled if the log_to_response parameter is set.

    *)
}

A response from CP-SAT. See the documentation in cp_model.proto.

val of_proto : model -> Cp_model.cp_solver_response -> t

Convert from the protocol buffer response format.

val pb_decode : model -> Pbrt.Decoder.t -> t

Convert from a protocol buffer decoder.

val of_input : model -> Stdlib.in_channel -> t

Read all the input data and decode.