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

cpmpy.transformations.to_cnf.flat2cnf(constraints)[source]

Converts from ‘flat normal form’ all logical constraints into Conjunctive Normal Form, including flattening global constraints that are is_bool() and not in supported.

What is now left to do is to tseitin encode:

  • BV with BV a BoolVar (or NegBoolView)

  • or([BV]) constraint

  • and([BV]) constraint

  • BE != BV with BE :: BV|or()|and()|BV!=BV|BV==BV|BV->BV

  • BE == BV

  • BE -> BV

  • BV -> BE

    We do it in a principled way for each of the cases. (in)equalities get transformed into implications, everything is modular.

    Arguments: - constraints: list[Expression] or Operator

cpmpy.transformations.to_cnf.to_cnf(constraints)[source]

Converts all logical constraints into Conjunctive Normal Form

Arguments: - constraints: list[Expression] or Operator - supported: (frozen)set of global constraint names that do not need to be decomposed