class ORTools::Sat::Model

Overview

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

Defined in:

ortools-sat/model.cr

Constructors

Instance Method Summary

Constructor Detail

def self.new #

[View source]

Instance Method Detail

def add_all_diff(vars : Array(Expressible)) #

Ensures all variables given take completely distinct values from each other


[View source]
def add_at_most_one(vars : Array(BoolVar)) #

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


[View source]
def 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.


[View source]
def 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.


[View source]
def add_bool_xor(vars : Array(BoolVar)) #

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


[View source]
def 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)


[View source]
def add_exactly_one(vars : Array(BoolVar)) #

Forces exactly one of the provided boolean variables to be true


[View source]
def 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


[View source]
def add_int_mod(target : Expressible, exprs : Array(Expressible)) #

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


[View source]
def 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.


[View source]
def add_max(target : Expressible, exprs : Array(Expressible)) #

Forces target to equal the max of all exprs


[View source]
def add_min(target : Expressible, exprs : Array(Expressible)) #

Forces target to equal the min of all exprs


[View source]
def add_none(vars : Array(BoolVar), enforcement_literals = [] of BoolVar) #

Forces all BoolVars provided to be false


[View source]
def add_not_all(vars : Array(BoolVar), enforcement_literals = [] of BoolVar) #

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


[View source]
def 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).


[View source]
def minimize(expr : Expressible, domain = [] of Int64, offset : Float64 | Nil = nil, scaling_factor : Float64 | Nil = nil) #

Create an objective to minimize


[View source]
def new_bool_var(name = "") #

Provides a BoolVar for boolean variables


[View source]
def new_int_var(min : Int, max : Int, name = "") #

Provides an IntVar for integer variables


[View source]
def 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


[View source]
def 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


[View source]
def 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.


[View source]
def valid? : Bool #

Returns true when the model passes OR-Tools validation.


[View source]
def validate : String #

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.


[View source]