Department of Computer Science

MUStICCa: MUS Extraction with Interactive Choice of Candidates

Existing algorithms for minimal unsatisfiable subset (MUS) extraction are defined independently of any symbolic information, and in current implementations domain experts mostly do not have a chance to influence the extraction process based on their knowledge about the encoded problem. The MUStICCa tool introduces a novel graphical user interface for interactive deletion-based MUS finding, allowing the user to inspect and influence the structure of extracted MUSes.
The tool is centered around an explicit visualization of the explored part of the search space, representing unsatisfiable subsets (USes) as selectable states. While inspecting the contents of any US, the user can select candidate clauses to initiate deletion attempts. The reduction steps can be enhanced by a range of state-of-the-art techniques such as clause-set refinement, model rotation, and autarky reduction.
MUStICCa compactly represents the criticality information derived for the different USes in a shared data structure, which leads to significant savings in the number of solver calls when multiple MUSes are explored. For automatization, our tool includes a reduction agent mechanism into which arbitrary user-defined deletion heuristics can be plugged.

Software

  • MUStICCa is a tool for interactively guiding the deletion-based MUS extraction algorithm. The tool is written entirely in Java, and builds on the Kahina framework for visualization and efficient data management. The package contains the tool, the required MiniSAT version, some example SAT instances and a User Guide. It is available for download as tar.gz (0.83 MB) file.
  • current version: from 07/11/2013
    • major improvements in stability
    • several minor bugs fixed
    • added the block view

Getting started with MUStICCa

  • Be sure to read the User Guide.
  • MUStICCa expects that the particular MiniSAT version is compiled and available in the system path. The source code of the required MiniSAT solver is present in the archives. After downloading and unzipping the archive, please compile MiniSAT by executing the makefile. After compiling MiniSAT, make sure that the MiniSAT folder is added to your system's path. Now you are able to start MUStICCa via "java -jar musticca.jar" and the interactive MUS extraction can begin! Simply load one of the example files we provide you with or any other unsatisfiable instance into the tool!

Related Publications