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.

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 via updates in PyPI. The latest version is 1.1.

Download

Examples

The module can be used quite simply, for example:

import boolopt

dnf = [[('notprop', 'a'), ('prop', 'b')], [('prop', 'b')]] # (!a && b) || b
opt = boolopt.optimize(dnf) # reduces to just b

A more full usage, using the internal classes:

import boolopt

plf = ('or', ('and', ('not', ('prop', 'a')), 
                     ('prop', 'b')), 
             ('prop', 'b'))
wff = boolopt.PLFtoWFF()(plf) # convert to positive-normal form
wtd = boolopt.WFFtoDNF()
dnf = wtd(wff)
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.