to_cnf

(function from pyomo.core.expr.cnf_walker)

pyomo.core.expr.cnf_walker.to_cnf(expr, bool_varlist=None, bool_var_to_special_atoms=None)[source]

Converts a Pyomo logical constraint to CNF form.

Note: the atoms AtMostExpression, AtLeastExpression, and ExactlyExpression require special treatment if they are not the root node, or if their children are not atoms, e.g.

atmost(2, Y1, Y1 | Y2, Y2, Y3)

As a result, the model may need to be augmented with additional boolean indicator variables and logical propositions. This function will raise ValueError if a BooleanVarList is not provided on which to store the augmented variables, and augmented variables are needed.

This function will return a list of CNF logical constraints, including:

  • CNF of original statement, including possible substitutions

  • Additional CNF statements (for enforcing equivalence to augmented variables)

In addition, the function will have side effects:

  • augmented variables are added to the passed bool_varlist

  • mapping from augmented variables to equivalent special atoms (see note above) with only literals as logical arguments