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	Var
Boolean operators	and([Var]), or([Var])	Operator, is_bool()
Boolean implication	Var -> Var	Operator, is_bool()
Boolean equality	Var == Var, Var == Constant	Comparison
Global constraint (Boolean)	global([Var]*)	GlobalConstraint, is_bool()

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

Numeric equality	Numexpr == Var, Numexpr == Constant	Comparison
Numeric disequality	Numexpr != Var, Numexpr != Constant	Comparison
Numeric inequality (>=,>,<,<=)	Numexpr >=< Var	Comparison

Numexpr:

Operator (non-Boolean) with all args Var/constant	+, *, /, mod, wsum	Operator, not is_bool()
Global constraint (non-Boolean)	Max, Min, Element	GlobalConstraint, not is_bool()

wsum:

Todo

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	Comparison
Implication	Boolexpr -> Var, Var -> Boolexpr	Operator, is_bool()

Boolexpr:

Boolean operators	and([Var]), or([Var])	Operator, not is_bool()
Boolean equality	Var == Var	Comparison
Global constraint (Boolean)	global([Var]*)	GlobalConstraint, is_bool()
Comparison constraint (see above)		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)

Type	Example	Notes
Satisfaction problem	None
Decision variable	Var	Operator, name sum
Linear	sum([Var]), wsum([Const],[Var])	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

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, csemap=None)

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

TODO, what built-in python error is best? RE TODO: we now have custom NotImpl/NotSupported

cpmpy.transformations.flatten_model.flatten_model(orig_model)

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

cpmpy.transformations.flatten_model.flatten_objective(expr, supported=frozenset({'sum', 'wsum'}), csemap=None)

• 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, csemap=None)

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, csemap=None)

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, csemap=None)

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])	Operator, not is_bool()
Boolean equality	Var == Var	Comparison
Global constraint (Boolean)	global([Var]*)	GlobalConstraint, is_bool()
Comparison constraint (see elsewhere)		Comparison

Result:

(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, csemap=None)

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()))

Result:

(base_expr, base_cons) with:

• base_expr: same as ‘expr’, but all arguments are variables

• base_cons: list of flat normal constraints