Follow
Hello all, looking for guidance! I want to "simplify Boolean expression" to create a minimal description of a boolean vector using pre-defined expressions, e.g. convert [0,0,1,1,0,1,1,1,0,0,0,0,0] into `fromEurope || (hasCar && likesMusic)` (made up example).
I've been looking into Z3 solver and `simplify` and patterns, but I'm not sure it can "go backwards", and I'm lost in the nomenclature and high-level math. E.g. would "weakest precondition"[1] apply to my case?
[1] https://en.wikipedia.org/wiki/Predicate_transformer_semantics
This has been sitting at the back of my head for a while, and I finally figured it out while seeing this image during a walk through a forest: I need two sets of model variables - "names" and "things" (both simply represented by a Bool in Z3py, True if "picked").
A "name" can imply picking multiple "things", and "things" must be picked by at least one name. Then I choose which "things" are picked (and crucially also which are not), and I let Z3 optimize to minimize the number of "names" used.