[CS] Generating pangrams using z3 SMT-solver

This is yet another illustration of (minimum) set cover problem: find a minimum number of words that contain all 26 a-z Latin letters.

A well-known pangram is The quick brown fox jumps over the lazy dog, usually used by font rendering software.

This code is almost similar by the previous, but disks are replaced with words and tracks/songs replaced with letters.

I've found that one need at least 600 most popular English words to construct a list of words that includes all 26 Latin characters:

 % ./set_cover.py top600.txt
...
Result: find example quick wave size joy bright
Words: 7
Phrase lenght (incl. spaces): 39
Chars used: abcdefghijklmnopqrstuvwxyz
Total chars used: 26

500 popular English words is not enough, because 'z' letter is missing in that list:

 % ./set_cover.py top500.txt
Result: draw night example always five quick object
Words: 7
Phrase lenght (incl. spaces): 43
Chars used: abcdefghijklmnopqrstuvwxy
Total chars used: 25

Funny thing, find best possible pangram using only 50 most popular Enlglish words (20 letters, which reflects most used letters in English):

 % ./set_cover.py top50.txt
Result: have this from by word can all up
Words: 8
Phrase lenght (incl. spaces): 33
Chars used: abcdefhilmnoprstuvwy
Total chars used: 20

Also, I can use a list of countries. This is the shortest:

 % ./set_cover.py countries.txt
...
Result: Bhutan Egypt Fiji Iraq Kosovo Mexico Swaziland
Words: 7
Phrase lenght (incl. spaces): 46
Chars used: abcdefghijklmnopqrstuvwxyz
Total chars used: 26

Funny thing, list of chemical elements is not enough to construct a 26-letter pangram, I've found only 24-letter one:

Result: Zinc Krypton Xenon Gold Bismuth Lawrencium Flerovium
Words: 7
Phrase lenght (incl. spaces): 52
Chars used: abcdefghiklmnoprstuvwxyz
Total chars used: 24

Short versions of chemical elements --- also without 2 letters:

Result: Ti Co Zn As Ru Xe Dy W Hg Po Bk Fm Lv
Words: 13
Phrase lenght (incl. spaces): 37
Chars used: abcdefghiklmnoprstuvwxyz
Total chars used: 24

Also, in Wikipedia I've found this:

With 35 letters, this is not the shortest pangram. Shorter examples include:

    "Waltz, bad nymph, for quick jigs vex." (28 letters)
    "Sphinx of black quartz, judge my vow." (29 letters)
    "How vexingly quick daft zebras jump!" (30 letters)
    "Pack my box with five dozen liquor jugs." (32 letters)

( src )

OK, I added these words to my test list to see, if my util can recreate these phrases. Yes, it can:

Result: Waltz bad nymph for quick jigs vex
Words: 7
Phrase lenght (incl. spaces): 34
Chars used: abcdefghijklmnopqrstuvwxyz
Total chars used: 26

Funny results are also produced:

Result: vexingly daft zebras jump Pack with liquor
Words: 7
Phrase lenght (incl. spaces): 42
Chars used: abcdefghijklmnopqrstuvwxyz
Total chars used: 26

But each tool has its limits. I couldn't use larger list of words (dictionaries). SMT solver is probably not the right tool for the job.

In "SAT/SMT by Example" I used OpenWBO MaxSAT solver to find minimal set of test files for larger problem: Ctrl-F: "Making smallest possible test suite using OpenWBO".

I don't know how practical this problem or not. (This is close to recreational math area.) But this could serve as another good example of (minimum) set cover problem.

All the files.

(the post first published at 20250325.)


List of my other blog posts.

Subscribe to my news feed,

Some time ago (before 24-Mar-2025) there was Disqus JS script for comments. I dropped it --- it was so motley, distracting, animated, with too much ads. I never liked it. Also, comments didn't appeared correctly (Disqus was buggy). Also, my blog is too chamberlike --- not many people write comments here. So I decided to switch to the model I once had at least in 2020 --- send me your comments by email to blog at yurichev dot com (don't forget to include URL to this blog post) and I'll copy&paste it here manually

Let's party like it's ~1993-1996, in this ultimate, radical and uncompromisingly primitive pre-web1.0-style blog and website.