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', name=None)[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

cpmpy.transformations.to_cnf.to_gcnf(soft, hard=None, name=None, csemap=None, ivarmap=None, encoding='auto', disjoint=True)[source]

Similar to make_assump_model, but the returned model is in (grouped) CNF. Separately the soft clauses, hard clauses, and assumption variables. Follows https://satisfiability.org/competition/2011/rules.pdf, however, there is no guarantee that the groups are disjoint.