Convert a 12-variable Boolean expression in disjunctive normal form (DNF) to conjunctive normal form (CNF) so that generating the truth table is NP-hard. Resulting CNF expression will be used in a student assignment.
Convert DNF to CNF is itself an NP-hard problem. If it were easy, SAT would not be NP. But I need a way to computationally convert DNF to CNF.
Possible solution: Wolfram|Alpha
Wolfram|Alpha is certainly able to convert DNF to CNF. Initial testing shows it works quite well for many variables, but it has a 200-character input limit. DNF expression is much longer than that.
Paid for annual Wolfram|Alpha subscription, hoping that would raise the character limit. Unsuccessful.
Applied for and was granted Wolfram|Alpha API access to try to get around the 200-character input limit. Unsuccessful. API error message is non-existent; it just silently refuses to run the query.
Possible solution: Mathematica
Download trial version of Mathematica and install on Mac. Success! Mathematica is able to convert DNF to CNF quickly. Twelve variables isn’t very many, anyway.
But Mathematica costs $500 to buy — a lot of money for a one-off problem I need to solve a couple times a year.
Possible solution: Karnaugh Maps
Learned that DNF can be converted to DNF using Karnaugh Maps. Just minimize the “zero” cells instead of the usual “one” cells. Invert the inputs. The result is a DNF expression. Seems easy enough.
Research K-map solvers. Most free ones are educational tools designed to show students how K-maps are solved. Because of the limited screen real estate, most can use at most four or five variables — nowhere near the twelve I need.
Possible solution: Roll my own K-Map solver
Getting desperate here. Spend a few hours thinking about how to solve K-Maps using only a truth table, as it would be silly to implement the actual 2D grid in a computer program. Came up with Quine-McCluskey algorithm on my own, so there’s that I guess.
But the Quine-McCluskey algorithm is also NP-hard. The number of prime implicants for 12 variables is as high as 3^n/3, or 177,147, so I see this is going nowhere fast.
Possible solution: Find a Q-M solver
Googled around for a Quine-McCluskey solver, ideally in Python. Found one called QM, referenced from the Wikipedia article. Ran it on my DNF expression. Waited about an hour, but still no results. Gave up.
Also found an optimized version of QM, but I’m already onto the next Possible Solution…
Possible solution: Symbolic computation package
Google around for a symbolic computation package for Python. Found one called Sympy. Install. Run. Plug in my DNF expression. Wait about 30 minutes with the CPU running at 100%. Give up.
Possible solution: Logic Friday
Learned that although DNF-to-CNF is NP-hard, some fine folks at UC Berkeley have discovered a heuristic approach that gives non-optimal but good-enough-for-me solutions. Originally for developing PLA devices at IBM, Logic Friday is a Windows application that implements the Espresso Heuristic Logic Minimizer.
Fire up a Windows VM, download, install Logic Friday. Plug in my DNF and, huzzah!, out pops a CNF within moments!
But.. It’s Windows. And non-scriptable. I’d like to be able to generate the DNF and convert to CNF in an automated fashion on a Linux box.
Working solution: Espresso on Linux
The Espresso Wikipedia page references a working copy of Espresso updated for ANSI C. (Note: this link is to the tar.gz file itself.)
Downloaded, installed on Linux.
Spent about six hours combing through the docs to get it to convert DNF to CNF (what it calls Product of Sum form). But output is still in a DNF formula.
Hack at the source code to get it to print CNF when the -pos command line argument is specified.
Finally get something to work:
$ espresso -pos -oeqntott mydnf.esp v13.0 = (d|!j|!l|!m) & (!a|!g|m) & (d|!k|l|m) & (c|!d|!e|!j|!l) & (c|d|i|k|m) & (b|!g|!j|m) & (!a|!i) & (!c|k|l|m) & (a|b|j|!m) & (!c|!e|!k|l|!m) & (!b|d|!e|!l|!m) & (a|c|!e|l) & (!b|j|!l|m) & (e|i|j|!k) & (!d|e|!k|l) & (!c|h) & (b|!d|i|k) & (!c|d|!i) & (!a|d|l) & (!b|!c|!l) & (!b|c|e|!j) & (c|e|k|!l) & (a|g) & (!c|e|!l|!m) & (!c|j|!k) & (d|h) & (e|j|l|!m) & (b|d|!g|!k) & (!a|!d|j) & (c|!d|!i) & (!a|!c) & (!b|c|!h|l) & (!d|g) & (!d|!e|k) & (d|!j|k) & (!i|!j) & (!e|g) & (h|!k) & (!f);
Total time spent on this problem: 12+ hours spread across several days. But in the end I got something that worked.
Didn’t get any grading done.