Convert boolean expressions to cnf (cpmpy.transformations.to_cnf)

Transform constraints to Conjunctive Normal Form (i.e. an and of or`s of literals, i.e. Boolean variables or their negation, e.g. from `x xor y to (x or ~y) and (~x or y)) using a back-end encoding library and its transformation pipeline.

cpmpy.transformations.to_cnf.to_cnf(constraints, csemap=None, ivarmap=None, encoding='auto')

Converts all constraints into Conjunctive Normal Form

Parameters:

• constraints – list[Expression] or Operator

• csemap – dict() used for CSE

• ivarmap – dict() used to map integer variables to their encoding (usefull for finding the values of the now-encoded integer variables)

• encoding – the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”)

Returns:

Equivalent CPMpy constraints in CNF, and the updated ivarmap

cpmpy.transformations.to_cnf.to_cnf_objective(expr, encoding='auto', csemap=None, ivarmap=None, supported=frozenset({}), supported_reified=frozenset({}))

Transform objective into weighted Boolean literals plus helper constraints.

Parameters:

• encoding – the encoding used for int2bool

• csemap – optional shared CSE cache (populated in-place)

• ivarmap – optional shared integer variable encoding dict (populated in-place)

• supported – supported global constraints for objective decomposition

• supported_reified – supported reified global constraints for objective decomposition

Returns:

(weights, xs, const, extra_cons)