How can I represent a self-enumerating pangram as a boolean function?

Question

The wiki article for self-enumerating pangrams states that they are computed using Binary Decision Diagrams. I've been reading about BDDs and from my understanding you need to represent some problem as a boolean function before you can construct a BDD for it.

How would I go about doing this?

I've been thinking about the problem for a few days now, and I'm pretty sure you could representing the input to the boolean function using a straightforward encoding:

10000 01010 01011 10101 ...
16A's 10B's 11C's 21D's ...

So for a pangram starting "sixteen A's, ten B's, eleven C's, twenty-one D's", you could represent it as 10000010100101110101...

This would mean that there are 26 * 5 = 130 variables in the boolean function, assuming you restrict the maximum frequency of a character to 32 occurrences.

The output should be whether the representation is a self-enumerating pangram or not, i.e. if the sentence describes its own set of frequencies.

To do this, a hash table (or several) must surely be required along the way.

So for the letter E, the hash table might begin:

one   -> 1
two   -> 0
three -> 2
four  -> 0
five  -> 1
...

Which in binary, might look like:

1   -> 1
10  -> 0
11  -> 10
100 -> 0
101 -> 1

If the summation of all lookups from the E hash table is equal to five input bits corresponding to E, then that section of the self-enumerating pangram is correct. If all sections are correct then the boolean function should yield 1, otherwise 0.

I'm fairly sure I could figure out how to carry out addition using a boolean function and how to check if two numbers are equal. I have no idea where to start with representing the hash table as a boolean function, however. Also, connecting all of the pieces together is likely to bewilder me.

Any thoughts? Ideas? Collaboration? I'd like to see where this goes.

Thanks in advance.

Axiomatic

has some leads: fatrazie.com/EWpangram.html – Ambrogio

This is a really interesting problem, that I've enjoyed thinking about for the past few hours. Personally I'd try and solve the problem with search, rather than try and mathematically solve it with boolean functions. I've had a look at some of the literature available on this link, and these papers put the way forward to solve it far more eloquently than I could. Hope that helps, and thanks very much for a few hours of very interesting thought. Dave – Tacitus

Very interesting indeed. Maybe you could find this document about Binary Decision Diagrams useful: voronkov.com/lics_doc.cgi?what=chapter&n=10 – Absolutism

it's an interesting problem, did you end up getting anywhere with this? I've tried reading through some of the papers but most of the older ones are hard to find/ don't seem to provide enough details. P.S. as far as I can tell your approach should work, I just wonder about possible optimisations that could be performed/whether any are necessary with modern computers (I'm guessing not) let me know if you ended up building this because if you didn't I may have to give it a shot myself. – Urogenous

Hey Mike. I didn't build this, but I did explore the area a bit more. If you think of the problem in terms of binary circuit design I find it more comprehensible. Through a combination of adders, or-gates, and-gates, etc, you could build up a complex gate that takes some encoded form of the pangram you'd like to test and outputs a single pin which is whether it is a self-enumerating pangram, or not. I think this would be easiest using a hardware descriptor language and then collapsing that out into a binary function. You could then feed that to one of many BDD programs. – Axiomatic

That probably wouldn't be optimal, but I'm sure there are algorithms for simplifying binary functions. If you want to collaborate on this project, give me a shout on GitHub at github.com/tuzz – Axiomatic

For anyone stumbling on this, I did get somewhere with this. I ended up reducing the problem of self-enumerating pangrams to the problem of boolean satisfiability and built a programming language around this idea which is here: sentient-lang.org – Axiomatic

Answer 1

The way I see it, the use of BDDs, as used in this context, are simply a way of representing and assisting in manipulating an expression used to evaluate, for example, if your sentence satisfies the requirements for being a self-enumerating pangram. There are rules for manipulating them in ways that are conceptually easier than those for manipulating statement in Boolean algebra, because they are easier to represent in that notation than in Boole's notation, the same way that a polynomial in 8000 variables is more difficult to deal with in its general form than in some other notation that represents where it came from and such. Computer algorithms exist for manipulating any of those four, so your best option is probably to look up and adapt one to your needs. You may find this document to be helpful.

Google may also be useful in finding additional resources.

Albertalberta