Currently, the boolalg.expr module implements conjunctive normal form (CNF), and disjunctive normal form (DNF). There are two other normal forms for sale on the interwebs.
The Algebraic Normal Form is an XOR of AND of variables. It relies heavily on properties of distribution over XOR, and the identity ~x <=> XOR(1, x). Given how simplification works, this normal form might be best implemented as a set of frozenset of int. Bonus that it's a canonical form!
Apparently, pyeda's "factored" form is also called Negation Normal Form, or NNF. I originally got the term "factor" from DeMicheli's Synthesis and Optimization of Digital Circuits. However, the term "factoring" is also used to describe a mathematical technique used during multi-level logic minimization, so a good idea to disambiguate. Proposal would be to change the factor method to to_nnf.
cjdrake
commented
9 years ago
Currently, the
boolalg.exprmodule implements conjunctive normal form (CNF), and disjunctive normal form (DNF). There are two other normal forms for sale on the interwebs.The Algebraic Normal Form is an
XORofANDof variables. It relies heavily on properties of distribution overXOR, and the identity~x <=> XOR(1, x). Given how simplification works, this normal form might be best implemented as asetoffrozensetofint. Bonus that it's a canonical form!Apparently, pyeda's "factored" form is also called Negation Normal Form, or NNF. I originally got the term "factor" from DeMicheli's Synthesis and Optimization of Digital Circuits. However, the term "factoring" is also used to describe a mathematical technique used during multi-level logic minimization, so a good idea to disambiguate. Proposal would be to change the
factormethod toto_nnf.factormethod toto_nnf