Convert reification constraints (cpmpy.transformations.reification)

Transformations that rewrite reified constraints as needed.

There are three types of reification (BV=BoolVar, BE=BoolExpr):

BV -> BE

single implication, from var to expression

BV <- BE

single implication, from expression to var

BE == BV

full reification / double implication (e.g. BV <-> BE)

Using logical operations, they can be decomposed and rewritten to each other.

This file implements:

only_bv_reifies()

transforms all reifications to BV -> BE or BV == BE

only_implies()

transforms all reifications to BV -> BE form

reify_rewrite()

rewrites reifications not supported by a solver to ones that are
cpmpy.transformations.reification.only_bv_reifies(constraints, csemap=None)[source]
cpmpy.transformations.reification.only_implies(constraints, csemap=None)[source]

Transforms all reifications to BV -> BE form

More specifically:

BV0 -> BV2 == BV3 :: BV0 -> (BV2->BV3 & BV3->BV2)
                  :: BV0 -> (BV2->BV3) & BV0 -> (BV3->BV2)
                  :: BV0 -> (~BV2|BV3) & BV0 -> (~BV3|BV2)
BV == BE :: ~BV -> ~BE, BV -> BE

Assumes all constraints are in ‘flat normal form’ and all reifications have a variable in lhs. Hence, only apply AFTER flatten_constraint() and only_bv_reifies().

cpmpy.transformations.reification.reify_rewrite(constraints, supported=frozenset({}), csemap=None)[source]

Rewrites reified constraints not natively supported by a solver, to a version that uses standard constraints and reification over equalities between variables.

Input is expected to be in Flat Normal Form without unsupported globals present. (so after flatten_constraint() and decompose_global()) Output will also be in Flat Normal Form

Boolean expressions and, or, and -> and comparison expression IV1==IV2 are assumed to support reification (actually currently all comparisons <op> in {‘==’, ‘!=’, ‘<=’, ‘<’, ‘>=’, ‘>’}, IV1 <op> IV2 are assumed to support reification BV -> (IV1 <op> IV2))

Parameters:

supported – a (frozen)set of expression names that support reification in the solver, including supported ‘Left Hand Side (LHS)’ expressions in reified comparisons, e.g. BV -> (LHS == V)