Convert to Flat Normal Form (cpmpy.transformations.flatten_model)

Flattening a model (or individual constraints) into ‘flat normal form’.

In flat normal form, constraints belong to one of three families with all arguments either constants, variables, list of constants or list of variables, and some binary constraints have a canonical order of variables.

Furthermore, it is ‘negated normal’ meaning that the ~ (negation operator) only appears before a Boolean variable (in CPMpy, absorbed in a ‘NegBoolView’), and it is ‘negation normal’ meaning that the - (negative operator) only appears before a constant, that is a - b :: a + -1*b :: wsum([1,-1],[a,b])

The three families of possible constraints are:

Base constraints: (no nesting)

  • Boolean variable

  • Boolean operators: and([Var]), or([Var]) (CPMpy class ‘Operator’, is_bool())

  • Boolean impliciation: Var -> Var (CPMpy class ‘Operator’, is_bool())

  • Boolean equality: Var == Var (CPMpy class ‘Comparison’)

    Var == Constant (CPMpy class ‘Comparison’)

  • Global constraint (Boolean): global([Var]*) (CPMpy class ‘GlobalConstraint’, is_bool())

Comparison constraints: (up to one nesting on one side)

  • Numeric equality: Numexpr == Var (CPMpy class ‘Comparison’)

    Numexpr == Constant (CPMpy class ‘Comparison’)

  • Numeric disequality: Numexpr != Var (CPMpy class ‘Comparison’)

    Numexpr != Constant (CPMpy class ‘Comparison’)

  • Numeric inequality (>=,>,<,<=): Numexpr >=< Var (CPMpy class ‘Comparison’)

Numexpr:

  • Operator (non-Boolean) with all args Var/constant (examples: +,*,/,mod,wsum)

    (CPMpy class ‘Operator’, not is_bool())

  • Global constraint (non-Boolean) (examples: Max,Min,Element)

    (CPMpy class ‘GlobalConstraint’, not is_bool()))

wsum: wsum([Const],[Var]) represents sum([Const]*[Var]) # TODO: not implemented yet

Reify/imply constraint: (up to two nestings on one side)

  • Reification (double implication): Boolexpr == Var (CPMpy class ‘Comparison’)

  • Implication: Boolexpr -> Var (CPMpy class ‘Operator’, is_bool())

    Var -> Boolexpr (CPMpy class ‘Operator’, is_bool())

Boolexpr:

  • Boolean operators: and([Var]), or([Var]) (CPMpy class ‘Operator’, is_bool())

  • Boolean equality: Var == Var (CPMpy class ‘Comparison’)

  • Global constraint (Boolean): global([Var]*) (CPMpy class ‘GlobalConstraint’, is_bool())

  • Comparison constraint (see above) (CPMpy class ‘Comparison’)

Reification of a comparison is the most complex case as it can allow up to 3 levels of nesting in total, e.g.:

  • (wsum([1,2,3],[IV1,IV2,IV3]) > 5) == BV

  • (IV1 == IV2) == BV

  • (BV1 == BV2) == BV3

Objective: (up to one nesting)

  • Satisfaction problem: None

  • Decision variable: Var

  • Linear: sum([Var]) (CPMpy class ‘Operator’, name ‘sum’)

    wsum([Const],[Var]) (CPMpy class ‘Operator’, name ‘wsum’)

The output after calling flatten_model() or flatten_constraint() will ONLY contain expressions of the form specified above.

The flattening does not promise to do common subexpression elimination or to automatically group commutative expressions (and, or, sum, wsum, …) but such optimisations should be added later.

TODO: update behind_the_scenes.rst doc with the new ‘flat normal form’ TODO: small optimisations, e.g. and/or chaining (potentially after negation), see test_flatten

cpmpy.transformations.flatten_model.flatten_constraint(expr)[source]

input is any expression; except is_num(), pure _NumVarImpl, or Operator/GlobalConstraint with not is_bool()

output: see definition of ‘flat normal form’ above.

it will return ‘Exception’ if something is not supported TODO, what built-in python error is best? RE TODO: we now have custom NotImpl/NotSupported

cpmpy.transformations.flatten_model.flatten_model(orig_model)[source]

Receives model, returns new model where every constraint is in ‘flat normal form’

cpmpy.transformations.flatten_model.flatten_objective(expr, supported=frozenset({'sum', 'wsum'}))[source]
  • Decision variable: Var

  • Linear: sum([Var]) (CPMpy class ‘Operator’, name ‘sum’)

    wsum([Const],[Var]) (CPMpy class ‘Operator’, name ‘wsum’)

cpmpy.transformations.flatten_model.get_or_make_var(expr)[source]

Must return a variable, and list of flat normal constraints Determines whether this is a Boolean or Integer variable and returns the equivalent of: (var, normalize(expr) == var)

cpmpy.transformations.flatten_model.get_or_make_var_or_list(expr)[source]

Like get_or_make_var() but also accepts and recursively transforms lists Used to convert arguments of globals

cpmpy.transformations.flatten_model.normalized_boolexpr(expr)[source]

input is any Boolean (is_bool()) expression output are all ‘flat normal form’ Boolean expressions that can be ‘reified’, meaning that

  • subexpr == BoolVar

  • subexpr -> BoolVar

are valid output expressions.

Currently, this is the case for subexpr: - Boolean operators: and([Var]), or([Var]) (CPMpy class ‘Operator’, is_bool()) - Boolean equality: Var == Var (CPMpy class ‘Comparison’) - Global constraint: global([Var]*) (CPMpy class ‘GlobalConstraint’) - Comparison constraint (see elsewhere) (CPMpy class ‘Comparison’)

output: (base_expr, base_cons) with:

base_expr: same as ‘expr’, but all arguments are variables base_cons: list of flat normal constraints

cpmpy.transformations.flatten_model.normalized_numexpr(expr)[source]

all ‘flat normal form’ numeric expressions…

Currently, this is the case for:

  • Operator (non-Boolean) with all args Var/constant (examples: +,*,/,mod,wsum)

    (CPMpy class ‘Operator’, not is_bool())

  • Global constraint (non-Boolean) (examples: Max,Min,Element)

    (CPMpy class ‘GlobalConstraint’, not is_bool()))

output: (base_expr, base_cons) with:

base_expr: same as ‘expr’, but all arguments are variables base_cons: list of flat normal constraints