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-implemented deletion heuristics can be plugged.