boolopt

boolopt is a Python module for optimizing propositional logic. It was written during my internship in Cape Town at NBN, South Africa’s National Bioinformatics Network; they used it for query optimization. The module provides a function optimize, which takes a disjunctive-normal formula (without intraclause contradictions and duplicates) and outputs an equivalent, minimal term. It uses the Quine-McCluskey algorithm for minimization.

There is an existing implementation, but I couldn’t get it to work — that’s why I wrote my own. (And now I, too, am in the Cheese Shop. Let the Battle of Quine-McCluskey begin!)

It’s worked instantaneously on all of the (small) examples I’ve thrown at it, but the method is NP-complete and involves building a truth-table — it’s EXPSPACE in the number of propositions.

I release it here under the NewBSD license: you can do whatever you want with the code so long as you leave the license and copyright information at the top.

New versions will be announced on the main site feed. The latest version is 1.0.

Download

Installation

Open up the archive wherever; it will create its own directory boolopt-1.0. Inside this directory there will be a file setup.py, a standard Python distutils setup file. Just run python setup.py install and you’re good to go!

To request support, bug fixes, and features, please send e-mail to .

Examples

The module can be used quite simply, for example:

  1. import boolopt
  2.  
  3. dnf = [[(‘notprop’, ‘a’), (‘prop’, ‘b’)], [(‘prop’, ‘b’)]] # (!a && b) || b
  4. opt = boolopt.optimize(dnf) # reduces to just b

A more full usage, using the internal classes:

  1. import boolopt
  2.  
  3. plf = (‘or’, (‘and’, (‘not’, (‘prop’, ‘a’)),
  4.                      (‘prop’, ‘b’)),
  5.              (‘prop’, ‘b’))
  6. wff = boolopt.PLFtoWFF()(plf) # convert to positive-normal form
  7. wtd = boolopt.WFFtoDNF()
  8. dnf = wtd(wff)
  9. opt = boolopt.QuineMcCluskey(lambda: wtd.props) # give a reference to pre-computed proposition set

Some weird spacing going on there…I need to check out my installation of SyntHihol. Probably my CSS.

Fun facts

Included in the distribution is a class ASTWalker, which automatically traverses tagged-tuple ASTs, dispatching to appropriate transformation and visitor methods. The automatic resolution of method names makes writing extensible visitors and transformers a snap. It’s also built to allow for overrides; any tag can be dispatched differently, plus the post-order recursion can be manually overridden.

*

a weasel in a hat