Prime Implicant Computation Using Satisfiability Algorithms

The computation of prime implicants has several and significant applications in different areas, including Automated Reasoning, Non-Monotonic Reasoning, Electronic Design Automation, among others. In this paper we describe a new model and algorithm for computing minimum-size prime implicants of propositional formulas. The proposed approach is based on creating an integer linear program (ILP) formulation for computing the minimumsize prime implicant, which simplifies existing formulations. In addition, we introduce two new algorithms for solving ILPs, both of which are built on top of an algorithm for propositional satisfiability (SAT). Given the organization of the proposed SAT algorithm, the resulting ILP procedures implement powerful search pruning techniques, including a non-chronological backtracking search strategy, clause recording procedures and identification of necessary assignments. Experimental results, obtained on several benchmark examples, indicate that the proposed mode...

• Type: Conference
• Year: 1997
• Where: ICTAI
• Authors: Vasco M. Manquinho, Paulo F. Flores, João P. Marques Silva, Arlindo L. Oliveira
• Keywords: Algorithms, Artificial Intelligence, ICTAI 1997, Minimum-size Prime Implicants, Prime Implicant