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

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