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.