Integration of solvers for determining minimal unsatisfiable subsets

The enumeration of the set of minimal unsatisfiable subsets of an inconsistent set of formulas is a reasoning task that occurs often when it comes to analysing inconsistent sets (as e.g. for inconsistency measurement). When using such components, it is required that at least one MUSEnumerator is explicitly configured as a default enumerator.

TweetyProject has built-in support for a naive approach to compute minimal unsatisfiable sets using the default SAT solver. However, whenever you perform a reasoning task that involves a MUS enumerator a warning message is printed out that no MUS enumerator is configured and the naive enumerator is used as a default. If you do not care about performance issues and only want to get rid of the warning message, you should configure the naive enumerator as your default enumerator solver explicitly. To do that, simply add the following lines somewhere before you invoke your reasoning task for the first time:

However, depending on your reasoning tasks it is recommend that you set another MUS enumerator as your default enumerator. TweetyProject also supports the integration of MARCO which is a Python-based command line tool for enumerating minimal unsatisfiable subsets. If you have MARCO installed in your system you can set it as your default MUS enumerator via:

If your favorite MUS enumerator is not supported, please have a look at the PlMusEnumerator.java interface in the org.tweetyproject.logics.pl.sat package and think about implementing a bridge yourself and contribute it to TweetyProject.