Module Sat.Constraint

Logical, linear, and other constraints.

Direct Form

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

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

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

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

val min : equality -> t

Max with negated target and expressions.

val abs : equality -> t

Max of the original expressions together with their negations.

Logical Constraints

val bool_or : Var.t_bool list -> t

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

val bool_and : Var.t_bool list -> t

All literals must be true. Same as And.

val bool_xor : Var.t_bool list -> t

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

val at_most_one : Var.t_bool list -> t

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

val exactly_one : Var.t_bool list -> t

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

val at_least_one : Var.t_bool list -> t

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

module WithArray : sig ... end

Constraints with arrays as arguments .

val 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

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

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

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

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

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

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

val 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

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

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

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

module Linear : sig ... end

Utilities

val to_string : t -> string

Return a string representing the linear expression.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for linear expressions.