package ortools

  1. Overview
  2. Docs
Build and export Google OR-Tools models

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (5)

Authors

  1. T
    Timothy Bourke <tim@tbrk.org>

Maintainers

  1. T
    Timothy Bourke <tim@tbrk.org>

Sources

ortools-9.15.0-3.tbz
sha256=2dfa5a221f07e7756afda6f23d066aae8ebb73254e201a44921f24e0491c5f7b
sha512=be451a999703a032444c632e0c87b4e391449cee0daa9f4837b0798fc7b8b1ce10abf7bc11dc7439a381a9281a7fb02b9239c75c3df0e4e70d2c690eeb8ae78c

doc/ortools/Ortools/Sat/index.html

Module Ortools.SatSource

Build a model for CP-SAT

Models

Sourcetype model

A CP-SAT model.

Sourceval 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.

Sourcemodule Domain : sig ... end

A subset of the integers.

Sourcemodule Var : sig ... end

Representation of integer variables and boolean literals.

Linear Expressions

Sourcemodule LinearExpr : sig ... end

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

include module type of LinearExpr.L

An empty linear expression.

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

A single variable.

Sourceval (*) : 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.

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

Multiplication of a linear expression by a constant.

Sourceval of_int : int -> LinearExpr.t

A constant linear expression.

Complement a boolean literal. Same as Var.not.

Constraints

Sourcemodule Constraint : sig ... end

Logical, linear, and other constraints.

Sourceval 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.

Sourceval 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

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

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

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

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

Hints

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

Suggest an initial solution for the given variable.

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

Suggest initial solutions for the given variables.

Sourceval clear_hints : model -> unit

Remove any initial solutions.

Assumptions

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

Add assumptions on boolean literals.

Sourceval clear_assumptions : model -> unit

Clear any assumptions on boolean literals.

Decision Strategies

Sourcetype 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.

Sourcetype 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.

Sourceval 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.

Sourceval 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

Sourcemodule Parameters : sig ... end

Encode a set of parameters as a protocol buffer.

Sourcemodule Response : sig ... end

A response from CP-SAT for a given problem.

Sourcetype 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.

Sourceval 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.

As for solve, but works directly with protocol buffers rather than through the structured interface.

Output

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.

Sourceval pb_output : model -> out_channel -> unit

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

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

Encode a model.