A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas

We tackle the problem of finding a smallest-cardinality MUS (SMUS) of a given formula. The SMUS provides a succinct explanation of infeasibility and is valuable for applications that rely on such explanations. We present a branch-and-bound algorithm that utilizes iterative MAXSAT solutions to generate lower and upper bounds on the size of the SMUS, and branch on specific subformulas to find it. We report experimental results on formulas from DIMACS and DaimlerChrysler product configuration suites.

• Type: Conference
• Year: 2005
• Where: SAT
• Authors: Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João P. Marques Silva, Karem A. Sakallah
• Keywords: DaimlerChrysler Product Configuration, Iterative Maxsat Solutions, SAT 2005, Smallest-cardinality Mus