Design and Implementation of Multiple-Context Truth Maintenance System with Binary Decision Diagram
Hiroshi G. Okuno, Osamu Shimokuni, Hidehiko Tanaka · Industrial and Engineering Applications of Artificial Intelligence and Expert Systems · 2022
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.