MUSTool

MUSTool enumerates minimal unsatisfiable subsets (MUSes) from unsatisfiable sets of constraints to identify the constraint subsets that cause unsatisfiability across SAT, SMT, and LTL domains.

Key Features:

• Online enumeration: Enumerates MUSes one at a time to produce partial results when complete enumeration is computationally infeasible.
• MUS enumeration algorithms: Implements the online MUS enumeration algorithms MARCO, TOME, and ReMUS.
• Domain support (SAT, SMT, LTL): Supports MUS enumeration across SAT, SMT, and LTL constraint domains without domain-specific modification.
• Extensibility: Provides an extensible architecture to add support for additional constraint domains.

Scientific Applications:

• Analysis of constraint unsatisfiability: Identifies minimal subsets that explain why a set of constraints is unsatisfiable.
• Constraint satisfaction and constraint solving research: Enables study and evaluation of MUS enumeration methods and constraint satisfaction problems.
• Cross-domain MUS enumeration: Applies MUS enumeration to instances formulated in SAT, SMT, and LTL to support analyses across multiple constraint domains.

Methodology:

Implements online MUS enumeration using the MARCO, TOME, and ReMUS algorithms to enumerate minimal unsatisfiable subsets one at a time.