class

ORTools::Sat::Model

Inherits Reference < Object

Model class contains all the variables and constraints that define the problem The variables and constraints are stored in the CpModelProto object The Class also provides all the methods used to add variables and define constraints

Constructors

Instance methods

add_all_diff(vars : Array(Expressible))

Ensures all variables given take completely distinct values from each other

Source
add_at_most_one(vars : Array(BoolVar))

Forces at most one of the provided boolean variables to be true

Source
add_bool_and(vars : Array(BoolVar), enforcement_literals = [] of BoolVar)

Forces all of the boolean variables to be true

When enforcement_literals are provided, this constraint will only be followed if all literals are true.

Source
add_bool_or(vars : Array(BoolVar), enforcement_literals = [] of BoolVar)

Forces at least one of the boolean variables to be true

When enforcement_literals are provided, this constraint will only be followed if all literals are true.

Source
add_bool_xor(vars : Array(BoolVar))

Forces an odd number of the provided boolean variables to be true

Source
add_constraint(constraint : LinearConstraint)

Implements a linear constraint in the form of a <= b or a == b.

E.g. model.add_constraint( 2x + 3y <= 44)

Source
add_exactly_one(vars : Array(BoolVar))

Forces exactly one of the provided boolean variables to be true

Source
add_int_div(target : Expressible, exprs : Array(Expressible))

Forces the target to equal exprs[0] / exprs[1]. The division is rounded towards zero. For exact integer division, use product constraint and place the target as an expr. E.g. a = b * target

Source
add_int_mod(target : Expressible, exprs : Array(Expressible))

Forces the target to be equal exprs[0] % exprs[1].

Source
add_int_prod(target : Expressible, exprs : Array(Expressible))

Forces the target to be equal to the product of the exprs. The product must fit in an int64 or the model will be invalid.

Source
add_max(target : Expressible, exprs : Array(Expressible))

Forces target to equal the max of all exprs

Source
add_min(target : Expressible, exprs : Array(Expressible))

Forces target to equal the min of all exprs

Source
add_none(vars : Array(BoolVar), enforcement_literals = [] of BoolVar)

Forces all BoolVars provided to be false

Source
add_not_all(vars : Array(BoolVar), enforcement_literals = [] of BoolVar)

Forces at least one of the provided boolean variables to be false

Source
maximize(expr : Expressible, domain = [] of Int64, offset : Float64 | Nil = nil, scaling_factor : Float64 | Nil = nil)

Create an objective to maximize

The solver only minimizes, so maximization is expressed by minimizing the negated expression. The reported objective_value is scaling_factor * (offset + sum(coeffs*vars)), so to keep it equal to the user's expression both the offset and the scaling factor must be negated as well (scaling_factor defaults to 1 when unset).

Source
minimize(expr : Expressible, domain = [] of Int64, offset : Float64 | Nil = nil, scaling_factor : Float64 | Nil = nil)

Create an objective to minimize

Source
new_bool_var(name = "")

Provides a BoolVar for boolean variables

Source
new_int_var(min : Int, max : Int, name = "")

Provides an IntVar for integer variables

Source
set_to_bool_and(target : BoolVar, vars : Array(BoolVar))

Creates and equivelence between target variable and the result of the logical AND of the vars

Source
set_to_bool_or(target : BoolVar, vars : Array(BoolVar))

Creates and equivelence between target variable and the result of the logical OR of the vars

Source
solve(max_time_in_seconds : Number | Nil = nil) : Solution

Attempts to solve

When max_time_in_seconds is provided, the search is capped at that many seconds. If the limit is reached the solver returns the best solution found so far (status FEASIBLE, or UNKNOWN if none was found) rather than running until it can prove optimality. Omitting it keeps the default behavior of searching until optimal/infeasible.

Source
valid?

Returns true when the model passes OR-Tools validation.

Source
validate

Validates the model against OR-Tools' own model checker.

Returns an empty string when the model is valid, otherwise a human readable description of the first problem found (e.g. an out-of-range variable reference). This is a cheap way to catch a malformed model before spending time in #solve.

Source