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.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!