Tweety
A comprehensive collection of Java libraries for logical aspects of artificial intelligence and knowledge representation
Home Libraries Downloads Documentation Web Interfaces Contact


Brought to you by




Supported by

back

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.

Tweety 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:

import net.sf.tweety.logics.commons.analysis.*;
import net.sf.tweety.logics.pl.sat.*;
...
PlMusEnumerator.setDefaultEnumerator(new
 NaiveMusEnumerator<PropositionalFormula>(SatSolver.getDefaultSolver()));

However, depending on your reasoning tasks it is recommend that you set another MUS enumerator as your default enumerator. Tweety 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:

PlMusEnumerator.setDefaultEnumerator(new MarcoMusEnumerator(pathToMarco));

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




back



Last updated 11.01.2016, Matthias Thimm