package ortools

  1. Overview
  2. Docs

Module Sat.ConstraintSource

Logical, linear, and other constraints.

Direct Form

This is the raw form of constraints accepted by CP-SAT. See below for more convenient functions.

Sourcetype equality = {
  1. target : LinearExpr.t;
  2. exprs : LinearExpr.t list;
}

An equality between a target linear expression and an operation, given externally, applied to multiple linear expression arguments. The target must be a (scaled) variable or constant, otherwise add raises Invalid_argument.

Sourcetype equality2 = {
  1. target : LinearExpr.t;
  2. arg1 : LinearExpr.t;
  3. arg2 : LinearExpr.t;
}

An equality between a target linear expression and a operation, given externally, applied to a linear expression and a constant argument. The target must be a (scaled) variable or constant, otherwise add raises Invalid_argument. Similarly, arg2 must be a (scaled) constant, but this cannot always be fully checked.

Sourcetype t =
  1. | Or of Var.t_bool list
    (*

    At least one of the literals must be true.

    *)
  2. | And of Var.t_bool list
    (*

    All literals must be true.

    *)
  3. | At_most_one of Var.t_bool list
    (*

    At most one literal is true. Sum literals <= 1.

    *)
  4. | Exactly_one of Var.t_bool list
    (*

    Exactly one literal is true. Sum literals == 1.

    *)
  5. | Xor of Var.t_bool list
    (*

    An odd number of literals is true.

    *)
  6. | Div of equality2
    (*

    Integer division by a constant.

    *)
  7. | Mod of equality2
    (*

    Integer modulo a constant.

    *)
  8. | Prod of equality
    (*

    Constrain a variable to equal the product of linear expressions.

    *)
  9. | Max of equality
    (*

    Constrain a variable to equal the maximum of a list of linear expressions.

    *)
  10. | Linear of LinearExpr.t * Domain.t
    (*

    Constrains a linear expression to a domain. Values of type Linear of lt are created by the (<=), (==), and similar operators.

    *)
  11. | All_diff of LinearExpr.t list
    (*

    Require that a list of (scaled) variables and constants have different values from each other.

    *)

The primitive constraints treated by CP-SAT.

Sourceval min : equality -> t

Max with negated target and expressions.

Sourceval abs : equality -> t

Max of the original expressions together with their negations.

Logical Constraints

Sourceval bool_or : Var.t_bool list -> t

At least one of the literals must be true. Same as Or.

Sourceval bool_and : Var.t_bool list -> t

All literals must be true. Same as And.

Sourceval bool_xor : Var.t_bool list -> t

An odd number of literals is true. Same as Xor.

Sourceval at_most_one : Var.t_bool list -> t

At most one literal is true. Sum literals <= 1. Same as At_most_one.

Sourceval exactly_one : Var.t_bool list -> t

Exactly one literal is true. Sum literals == 1. Same as Exactly_one.

Sourceval at_least_one : Var.t_bool list -> t

At least one of the literals must be true. Same as Or.

Sourcemodule WithArray : sig ... end

Constraints with arrays as arguments .

Sourceval implication : Var.t_bool -> Var.t_bool -> t

Logical implication between two literals. (implication a b is the same as Or [(Var.not a); b] .)

Integer Relations

Sourceval multiplication_equality : 'a Var.t -> LinearExpr.t list -> t

Constrain a variable to equal the product of linear expressions. Slightly less general than Prod since the left-hand-side may also be a scaled variable or a constant. multiplication_equality v [x y z] means v = x * y * z.

Sourceval division_equality : 'a Var.t -> LinearExpr.t -> int -> t

Integer division by a constant. Slightly less general than Div, since the left-hand-side may also be a scaled variable or a constant. division_equality x e c means x = e // c.

Sourceval modulo_equality : 'a Var.t -> LinearExpr.t -> int -> t

Integer modulo a constant. Slightly less general than Mod, since the left-hand-side may also be a scaled variable or a constant. modulo_equality x e c means x = e % c.

Sourceval max_equality : 'a Var.t -> LinearExpr.t list -> t

Constrain a variable to equal the maximum of a list of linear expressions. Slightly less general than Max since the left-hand-side may also be a scaled variable or a constant.

Sourceval min_equality : 'a Var.t -> LinearExpr.t list -> t

Slightly less general than min since the left-hand-side may also be a scaled variable or a constant.

Sourceval abs_equality : 'a Var.t -> LinearExpr.t list -> t

Slightly less general than abs since the left-hand-side may also be a scaled variable or a constant.

Sourceval all_different : LinearExpr.t list -> t

Require that a list of (scaled) variables and constants have different values from each other. Same as All_diff.

Linear Constraints

Sourceval of_expr : LinearExpr.t -> lb:int -> ub:int -> t

A Linear constraint: of_expr e lb ub means lb <= e <= ub.

Sourceval in_domain : LinearExpr.t -> Domain.t -> t
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.nto.

Sourcemodule Linear : sig ... end

Utilities

Sourceval to_string : t -> string

Return a string representing the linear expression.

Sourceval pp : Format.formatter -> t -> unit

Pretty-printer for linear expressions.