Implicit enumeration of prime implicates in Truth Maintenance System
(TMS) is investigated.  CMS (Clause Management System), an extension
of Assumption-based TMS (ATMS), that accepts any type of justification
has a burden to compute all prime implicates, since its complexity is
NP-complete.  To improve the performance of multiple-context TMS such
compact representation of boolean functions.  In this paper, we
propose a BDD-based Multiple-context TMS (BMTMS) and present the
design and implementation of interface between TMS and BDD.  The
interface provides high level specifications of logical formulas, and
has mechanisms to schedule BDD commands to avoid combinatorial
explosions in constructing BDDs.  In BMTMS, most TMS operations are
carried out without enumerating all prime implicates.