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

Meta-transformation for obtaining a CNF from a list of constraints.

Converts the logical constraints into disjuctions using the tseitin transform, including flattening global constraints that are is_bool() and not in supported.

Note

The transformation is no longer used by the SAT solvers, and may be outdated. Check CPM_pysat.transform for an up-to-date alternative.

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