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