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

Converts the logical constraints into disjuctions using the tseitin transform,

including flattening global constraints that are is_bool() and not in supported.

Other constraints are copied verbatim so this transformation can also be used in non-pure CNF settings

The implementation first converts the list of constraints to ‘flat normal form’, this already flattens subexpressions using auxiliary variables.

What is then left to do is to tseitin encode the following into CNF:

  • 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

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.

Parameters:

constraints – list[Expression] or Operator

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

Converts all logical constraints into Conjunctive Normal Form

Parameters:

  • constraints – list[Expression] or Operator

  • supported – (frozen)set of global constraint names that do not need to be decomposed