Abstract
The explanation of infeasibilities formed in Minimal Unsatisfiable Subformulas (MUSes) is a core task in the analysis of over-constrained Boolean formulas. A wide range of applications necessitate MUS detection including knowledge-based validation, software design, verification and error diagnosis in digital VLSI circuits. Consequently, various enhanced algorithms for determining MUS have been utilized for solving Maximum Satisfiability algorithms and Conjunction Normal Form (CNF) redundancies. Three enhancements are proposed in this paper. The first is a CPU-GPU algorithm for computation of Minimal Correction Subsets (MCSes) optimized for NVIDIA General Purpose Graphics Processing Unit paradigm. The proposed algorithm of generating all MCSes from the encoded CNF instance was developed using our parallel SSGPU solver and implemented using CUDA. The second enhancement is an algorithm for MUS computation based on auto-reduction of the enhanced MCSes for faster MUS detection. The third improved algorithm is for computing MUS directly without using MCSes. The two proposed algorithms outperform techniques as they could locate and explain design faults in digital VLSI circuits in earlier stages of IC design flow. The second proposed routine of MUS extraction was performed by avoiding a non-critical step in calling the SAT solver during MUS computation, leading to improving the performance of the MUS extraction algorithm. The third proposed mechanism for direct extraction of MUS was optimized by reducing the required SAT-solver calls using a classification of clauses in the input formula. Comparative analysis of the proposed algorithm against the Compute All Minimal Unsatisfiable Subsets (CAMUS) algorithm determined 1.54 x faster detection of MUS using ISCAS'85, ISCAS'89 and synthetic benchmarks. Also, the third algorithm for direct MUS computation delivers 17.05 x faster than shrinking algorithm used in MUST (minimal unsatisfiable subset) tool using ISCAS'85 and synthetic benchmarks. Moreover, it was observed that the CPU-GPU algorithm for MCSes computation based on the SSGPU solver delivered 1.92 x faster than its conventional counterpart, based on CUD@SAT equivalent on GPU using ISCAS'85, ISCAS'89 and synthetic Benchmarks.