Expression simplification?

[tyt2y3]

I could not find relevant methods in the docs. Just to clarify, this library does not have built in functions for boolean expression simplification / optimization with techniques like common term extraction? What would be the design or technical reason?

[welchbj]

Expression minimization functionality is definitely on my road map for this project and one of the new interfaces I hope to put together soon. The techniques I am hoping to add to the library first would be a pure-Python implementation of the Quine-McCluskey algorithm and a C-wrapper around the Espresso minimization tool.

I can definitely see the benefits in including lexical approaches to simplifying BooleanExpression objects, which would obviate the need to walk all input combinations to produce an exhaustive truth table, required by absolute minimization techniques.

Other planned improvements to the library that could assist in speeding up the minimization of increasingly complex expressions might include the introduction of the Tseytin transformation to the transformation api, which would yield linear expansion of transformations to CNF, as opposed to the near-exponential behavior in the current to_cnf transformation logic; however, this implementation detail should remain invisible to the Espresso and other CNF-requiring functionality (like the PicoSAT interface).

If you have any input on the design or implementation of these features to be added to the library, please feel free to add any thoughts within this issue. I'll label it appropriately if you choose to do so. I'm curious as to your possible use case for this library. Would you plan on using it as a learning/teaching tool, or have you applied it to any real combinational logic work?

Thanks for your interest and taking the time to open an issue. Please feel free to ask any questions or contribute any additional ideas.

[tyt2y3]

Hi, the intention was somewhat research / educational.
When I look at a tree representation, I immediately think of some algorithms that simplify the syntax tree.
such that,

AB + AB' = A(B+B') = A

and so on to be applied repeatedly until no further simplification can be made. Kind of the exercise we all learn in Logic 101.
If greedily done, it is not guaranteed to give optimal solutions, but I am interested how well such a method can do in practice.

[welchbj]

The type of transformation you describe is something that I am trying to open up to the user through the new transformation composition interface I've been working on lately, namely the tt_compose function.

Once I add one more "built-in" transformation capable of factoring out a common factor in ANDed and ORed expressions, as in the example you provided, implementing the example that you provided should be as simple as doing something like:

>>> f = tt_compose(factor_common_operand, apply_inverse_law)
>>> f
<ComposedTransformation [factor_common_operand -> apply_inverse_law]>
>>> f('(A && B) || (A && ~B)')
<BooleanExpression "A">

Note that in this code snippet, the factor_common_operand transformation does not yet exist in the library, but I think this is the only missing piece preventing the implementation of your example.