\documentclass[10pt,a4paper]{article}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{url}
\author{Andreas Sekine}
\title{Math 480 Project}
\date{June 6, 2008}
\setlength{\topmargin}{0in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\setlength{\textheight}{9in}
\setlength{\oddsidemargin}{0in}
\setlength{\textwidth}{6in}
\begin{document}
\begin{flushright}
Andreas Sekine \\
Math 480A \\
Final Project
\end{flushright}
\begin{center} \begin{Large}
Boolean Formulas (Propositional Calculus) in Sage
\end{Large} \end{center}
\section{Background}
\subsection{Simplification Methods}
\indent\indent There are a few widely used algorithms for minimizing Boolean formulas, most
notable of which are the \textbf{Quine-McCluskey} algorithm, and the \textbf{Espresso}
method. Both work by taking a Boolean formula and compute an equivalent expression
using simpler operators and/or fewer terms. Both methods return a solution expressed in
sum-of-products terms, a formula involving \textit{and} terms \textit{or}'ed together.
The computational and spatial complexity of Quine-McCluskey is exponential, and can quickly
become unreasonable for complex formulas involving many variables. It is guaranteed to find
a solution with the minimum number of terms.
The Espresso method uses heuristics to minimize a formula much more quickly, however it does
not guarantee the simplest form of the expression. It typically finds solutions that are
relatively short, and much more quickly than Quine-McCluskey.
\section{Logic in Sage (The \texttt{logic} Module)}
\subsection{Current Release}
As of version 3.0.1, the logic module relies the {\tt SymbolicLogic} class to deal with
Boolean logical statements and expressions. It has several function stubs, such as
{\tt prove, simplify,} and {\tt combine}.
While {\tt SymbolicLogic} did implement basic Boolean operations and functions, there were
some poor design choices and holes left that left much to be desired. For example, it used
the strings \textit{"OPAREN"} and \textit{"CPAREN"} to internally store parentathes, and
used the name \texttt{eval} for evaluating a statement, which is generally bad style since
python has a built in eval function.
\subsection{Active Development}
The logic module in sage is currently undergoing active development. The sage ticket \\
\url{http://sagetrac.org/sage_trac/ticket/545} shows the current progress. There were
many significant changes to the logic module:
\begin{itemize}
\item The code was refactored into several files. Before it all resided in
\textit{logic.py}, and now is sepp up according to functionality. For example,
the parsing of the statement now is the responsibility of \textit{logicparser.py},
and \textit{boolformula.py} holds the related class
\item The names were changed. Instead of being called through \texttt{SymbolicLogic},
a boolean function is initialized through the \texttt{propcalc} module, and uses
the \texttt{BooleanFormula} class.
\item Boolean formulas are stored internally in a tree structure now
\end{itemize}
\subsubsection{Simplification}
\texttt{BooleanFormula} objects in sage have a \texttt{simplify} method that can be
used to reduce expressions to their minterms (sum-of-products form) by using the
Quine-McCluskey algorithm. This is accomplished using the \textbf{boolopt} package
developed by Michael Greenberg (\url{http://www.weaselhat.com/boolopt/}).
\subsubsection{Suggested Improvements}
Ticket 545 contains a patch that completely reworked the logic module, and is currently
awaiting review. After inspection it seems that the patch still issues that need to be
addressed.
\begin{itemize}
\item It seems like there should be a way to evaluate a given
\texttt{BooleanFormula} with specified inputs. It may possible by calling
\textit{booleval.eval\_formula)}, however there should probably be an interface
for such basic functionality, without having to resort to making an entire
truth table.
\item \texttt{propcalc.formula} includes the following code:
\begin{verbatim}
#verify the syntax
f.truthtable(0, 1)
\end{verbatim}
The truthtable construction doesn't do any (direct) error checking, and won't
throw any helpful error messages. Meanwhile the logicparser does plenty of
syntax checking for valid input -- is the truthtable call necessary?
\item Currently \textit{boolopt.py} is imported by propcalc by calling
\texttt{sys.path.append('boolopt-1.1')}, and then importing the module. Applying the
patch directly didn't work, and python complained about not finding the boolopt
import. I had to fix it by copying \textit{boolopt.py} to the parent
directory (sage/logic).
\item BooleanFormula.\_latex\_ doesn't work properly, as it doesn't escape any latex
reserved characters. Particularly the symbols \verb1&, ^ and ~1.
It may be possible to enter the latex formula in verbatim block, however this
should probably be mentioned in the docstring if it's to be the case
\item \texttt{BooleanFormula\_\_eq\_\_} has very naive behavior - it just performs
literal comparison of trees, and you get behavior like the following:
\begin{verbatim}
sage: p = propcalc.formula("a|b")
sage: q = propcalc.formula("b|a")
sage: p == q
False
\end{verbatim}
This may be the desired behavior, but then maybe there should be a method
\texttt{equivalent} that can find out if something is logically equivalent.
This presents certain challenges, such as
\item The docstring examples for \texttt{BooleanFormula.convert\_expression} and
\texttt{BooleanFormula.convert\_cnf} are the same, and yet the functions
do different things. Both contain the following:
\begin{verbatim}
EXAMPLES:
sage: import propcalc
sage: s = propcalc.formula("a^b<->c")
sage: s.convert_cnf_recur() #long time
(a|a)&(b|a)&(a|c)&(b|c)
\end{verbatim}
\item There are a few methods that would be nice for a logic module to have, such
as \texttt{is\_tautology} or \texttt{is\_contradition}. These would not be hard
to implement, just an enumeration over possible inputs until a counterexample
is found, or all inputs have been exhastively searched.
\item \textit{booleval.py} contains a few very poorly written methods:
\texttt{eval\_ifthen\_op} and \texttt{eval\_iff\_off}. The body of
eval\_ifthen\_op, for example, is:
\begin{verbatim}
if(lval == False and rval == False):
return True
elif(lval == False and rval == True):
return True
elif(lval == True and rval == False):
return False
elif(lval == True and rval == True):
return True
\end{verbatim}
which could be simplified to \verb1 (not lval) or rval 1
\item \texttt{BooleanFormula.simplify} would sometimes cause system hangs, even
on small numbers of variables. I Was able to establish that this was only when the
formula involed \verb1<->, ^, and ->1. It's possible my test code was incorrect,
but then one would hope the parser would have caught that, and rejected my
attempt at created a BooleanFormula object. It could also be the
\texttt{BooleanFormula.reduce\_op} method, which is responsible for converting
all \verb1<->, ^, and ->1 into \verb1&, | and ~1.
\end{itemize}
\section{The Quine-McCluskey Algorithm}
The Quine-McCluskey Algorithm (also known as the \textbf{Prime Implicant} method is
guaranteed to find a minimized equivalent form of a boolean expression. Minimized means
the smallest number of sum-of-product terms, that is, a series of \textit{and} terms
\textit{or}'ed together. This method is often chosen for automation because it is a
relatively simple process. The steps are as follows:
\begin{enumerate}
\item Iterate over all possible inputs to the boolean expression, and build up a
table of the combinations that result in an evaluation to $true$, grouping the
table entries by the number of $true$'s they have as in. These combinations are
known as \textit{minterms}.
Note: because each input variable has 2 possible inputs, this means there are a
possible $2^n$ input combinations for $n$ variables.
\item Compare each element of each group with the elements of the neighboring group.
If there are any elements in a neighboring group that only differs by a single
input, you know you can simplify away that variable, since leaving it out of the
term covers both cases (if the input had been $T$ or $F$). This variable entry is
replaced with a "$-$" as a place holder, which is known as a \textit{dont-care}.
\item Iterate over the entire column, putting terms created with don't cares in the next
column, until there are no more combinations to be formed.
\item Repeat this process for the newly created column: look for terms that differ
by only 1 input (the dont-care's have to be matched too -- only one variable of
input is allowed to differ), and comtinue to make new columns that include more
dont-care terms.
\item Once no more terms can be combined, create a list out of every term that was
unable to combine with any other terms (regardless of which column they ended up
in). These are known as \textit{prime implicants}. Mark in the table which minterms
are covered by which prime implicants.
\item Create a \textit{prime implicant table}, with the prime implicants along the
left (the first column), and the minterms along the top.
\item Find the smallest number of implicants that will cover all the minterms - this
is done by first figuring out which (if any) prime implicants exclusively provide
cover for any minterms. Mark these as necessary for your final solution; these are
known as \textit{essential prime implicants}. Then successively try combinations
of the remaining prime implicants until the smallest combination is found that covers
all of the minterms
\end{enumerate}
\end{document}