Theorem Proving with Binary Decision Diagrams

Hiroshi G. Okuno (NTT Basic Research Laboratories)

Binary Decision Diagrams (BDDs) are compact representations
of boolean functions (propositional logic).  We first review
BDDs and describe their application to the Magic Square
Problem.  The problem is encoded as a set of constraints and
each constraint is specified by (arithmetic) logic
expression.  The BDD for all the solutions is constructed by
taking logical-and's of all the constraints.  In
constructing BDDs, the order of constraints is critical to
avoid combinatorial explosions.  Since the resulting BDD
contains all the solutions implicitly, the solutions are
extracted by enumerating all the paths from the root of BDD
to the terminal node 1.  However, various capabilities are
possible without enumerating the solutions.  For example,
the theorem that the sum of the inner four squares of the
Magic Square of order 4 (4 x 4 chess board) is the same as
that of any column, row or diagonal can be proved by
constructing a BDD for the theorem.

Since a (standard) BDD contains logical relations between
propositional symbols, its size is much larger than that of
simple representation of combination sets.  Standard BDDs
can represent combination sets by logical functions, but
such representations are not canonical.  We introduce a new
kind of BDD called 0-suppressed-BDD (0-sup-BDD) to represent
a combination set uniquely.  The following two
combination-set operations are introduced:

\begin{itemize}

\item {\it Restriction}  ($F \bigtriangleup C $):
\(
F \bigtriangleup C \equiv \{x \in F | \exists y \in C, x \supseteq y\}
\)

\item {\it Exclusion} ($F \bigtriangledown C$):
\(
F \bigtriangledown C \equiv F - (F \bigtriangleup C) 
\)
\end{itemize}

Some theorems concerning combination-set operations are used
to reorder the order of applying operations to avoid the
combinatorial explosions.  The main differences of 0-sup-BDD
from standard BDDs in solving the Magic Square problems and
N-Queen problems are (1) the size of BDD is by ten times
smaller, and (2) the same constraints may be applied
repeatedly.  The latter property is due to the theorem that
elements of constraint $C$ that are irrelevant to $F$ are
ignored in restriction and exclusion operations.