Module Ortools.Sat

Build a model for CP-SAT

Models

type model

A CP-SAT model.

val make : ?nvars:int -> ?name:string -> unit -> model

Create an empty model. The nvars argument optionally specifies the expected number of variables, which determines the size and growth of internal data structures. The optional name argument is useful for debugging and logging applications with multiple models.

module Domain : sig ... end

A subset of the integers.

module Var : sig ... end

Representation of integer variables and boolean literals.

Linear Expressions

module LinearExpr : sig ... end

Linear expressions are used in linear constraints and to specify objectives.

include module type of LinearExpr.L
val zero : LinearExpr.t

An empty linear expression.

val var : 'a Var.t -> LinearExpr.t

A single variable.

val (*) : int -> 'a Var.t -> LinearExpr.t

A single term.

Concatenatation of two linear expressions.

Concatenatation of the left expression with the negation of the right expression.

val scale : int -> LinearExpr.t -> LinearExpr.t

Multiplication of a linear expression by a constant.

val of_int : int -> LinearExpr.t

A constant linear expression.

val not : Var.t_bool -> Var.t_bool

Complement a boolean literal. Same as Var.not.

Constraints

module Constraint : sig ... end

Logical, linear, and other constraints.

val add : model -> ?name:string -> ?only_enforce_if:Var.t_bool list -> Constraint.t -> unit

Add a constraint to the model, with an optional name. The constraint is conditional if the only_enforce_if argument is a non-empty list of boolean literals.

val add_implication : model -> ?name:string -> Var.t_bool list -> Var.t_bool list -> unit

Adds an implication constraint to the model. add_implication m lhs rhs = add m ~only_enforce_if:lhs (Constraint.And rhs)

include module type of Constraint.Linear

A linear constraint: lhs <= rhs.

A linear constraint: lhs >= rhs.

A linear constraint: lhs < rhs.

A linear constraint: lhs > rhs.

A linear constraint: lhs == rhs.

A Linear constraint: lhs != rhs.

Objectives

val maximize : model -> LinearExpr.t -> unit

The linear expression to maximize. Any existing objective is replaced.

val minimize : model -> LinearExpr.t -> unit

The linear expression to minimize. Any existing objective is replaced.

Hints

val add_hint : model -> 'a Var.t -> int -> unit

Suggest an initial solution for the given variable.

val add_hints : model -> ('a Var.t * int) list -> unit

Suggest initial solutions for the given variables.

val clear_hints : model -> unit

Remove any initial solutions.

Assumptions

val add_assumptions : model -> Var.t_bool list -> unit

Add assumptions on boolean literals.

val clear_assumptions : model -> unit

Clear any assumptions on boolean literals.

Decision Strategies

type variable_selection_strategy =
  1. | ChooseFirst
    (*

    The first variable in the list that is not fixed.

    *)
  2. | ChooseLowestMin
    (*

    The variable that might take the lowest value.

    *)
  3. | ChooseHighestMax
    (*

    The variable that might take the highest value.

    *)
  4. | ChooseMinDomainSize
    (*

    The variable having the fewest feasible assignments.

    *)
  5. | ChooseMaxDomainSize
    (*

    The variable having the most feasible assignments.

    *)

Specifies branching decisions on variables.

type domain_reduction_strategy =
  1. | SelectMinValue
    (*

    Try to assign the smallest value.

    *)
  2. | SelectMaxValue
    (*

    Try to assign the largest value.

    *)
  3. | SelectLowerHalf
    (*

    Branch to the lower half of the domain.

    *)
  4. | SelectUpperHalf
    (*

    Branch to the upper half of the domain.

    *)
  5. | SelectMedianValue
    (*

    Try to assign the median value.

    *)
  6. | SelectRandomHalf
    (*

    Randomly select either the lower or the upper half of the domain.

    *)

Specifies branching decisions on domains.

val add_decision_strategy : model -> 'a Var.t list -> variable_selection_strategy -> domain_reduction_strategy -> unit

Controls how the solver branches when no further deductions are possible. The selection and reduction strategies are applied to the given list of variables in order. Adding a new decision strategy replaces any existing one.

val add_decision_strategy_with_exprs : model -> LinearExpr.t list -> variable_selection_strategy -> domain_reduction_strategy -> unit

Controls how the solver branches when no further deductions are possible. The selection and reduction strategies are applied to the given list of expressions. Adding a new decision strategy replaces any existing one.

Solutions

module Parameters : sig ... end

Encode a set of parameters as a protocol buffer.

module Response : sig ... end

A response from CP-SAT for a given problem.

type raw_solver = ?observer_pb:(string -> unit) -> parameters_pb:string -> model_pb:string -> unit -> string

An interface for invoking CP-SAT. This function is passed protocol buffers for the parameters and the model and should return a protocol buffer for the response.

val solve : raw_solver -> ?observer:(Response.t -> unit) -> ?parameters:Parameters.t -> model -> Response.t

Calls a raw_solver with encoded versions of the parameters and model and returns the decoded response. If a (feasible solution) observer is given, it will be invoked for each feasible solution. Set Sat_parameters.sat_parameters.enumerate_all_solutions, to observe them all.

Output

val to_proto : model -> Cp_model.cp_model_proto

Converts a model to a protocol buffer. NB: copying is minimized, so the returned data structure shares some (mutable) data structures with the model. I.e., it becomes invalid if the model is changed.

val pb_output : model -> Stdlib.out_channel -> unit

Send the model to the output channel as a protocol buffer.

val pb_encode : model -> Pbrt.Encoder.t -> unit

Encode a model.