This tool is intended for solving the Smallest Minimal Unsatisfiable Subset (smallest MUS, SMUS) problem. Given an unsatisfiable CNF formula in DIMACS, it finds a smallest unsatisfiable subset of clauses using the CEGAR-based 2QBF approach.

Authors: Alexey Ignatiev, Mikolas Janota
Contributor: Joao Marques-Silva

Download: Linux X86-64 binary, MacOS X Mavericks X86-64 binary,