Package | Description |
---|---|
net.sf.tweety.logics.commons.analysis | |
net.sf.tweety.logics.pcl.analysis | |
net.sf.tweety.logics.pl.sat |
Modifier and Type | Interface and Description |
---|---|
interface |
MusEnumerator<S extends Formula>
Interface for classes enumerating MUSes (minimal unsatisfiable sets) and
MCSs (maximal consistent sets).
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractBeliefSetConsistencyTester<S extends Formula>
Classes extending this abstract class are capable of testing
whether a given belief set is consistent.
|
class |
AbstractMusEnumerator<S extends Formula>
Abstract implementation for MUes enumerators.
|
class |
NaiveMusEnumerator<S extends Formula>
A simple approach to compute minimal inconsistent subsets and maximal
consistent subsets by exhaustive search.
|
Modifier and Type | Field and Description |
---|---|
private BeliefSetConsistencyTester<S> |
DrasticInconsistencyMeasure.consTester
The consistency tester used for measuring.
|
private BeliefSetConsistencyTester<S> |
NaiveMusEnumerator.tester
Used for making consistency checks.
|
Constructor and Description |
---|
DrasticInconsistencyMeasure(BeliefSetConsistencyTester<S> consTester)
Creates a new drastic inconsistency measure.
|
NaiveMusEnumerator(BeliefSetConsistencyTester<S> tester)
Creates a new naive MusEnumerator that uses the given consistency tester.
|
Modifier and Type | Class and Description |
---|---|
class |
PclDefaultConsistencyTester
This class is capable of checking whether a given conditional knowledge base
is consistent by searching for the root of some equivalent multi-dimensional function.
|
Modifier and Type | Class and Description |
---|---|
class |
LingelingSolver
A wrapper for the Lingeling SAT solver
(tested with Lingeling version ats1 ce8c04fc97ef07cf279c0c5dcbbc7c5d9904230a).
|
class |
MarcoMusEnumerator
Implements a MUs enumerator based on MARCO (http://sun.iwu.edu/~mliffito/marco/).
|
class |
MimusMusEnumerator
Implements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).
|
class |
PlMusEnumerator
This abstract class models a MUS enumerator for propositional logic, i.e.
|
class |
Sat4jSolver
Uses the Sat4j library for SAT solving (note that currently only the light version is used).
|
class |
SatSolver
Abstract class for specifying SAT solvers.
|
class |
SimpleDpllSolver
This class provides a simple reference implementation of the DPLL (Davis–Putnam–Logemann–Loveland)
algorithm for satisfiability testing, see e.g https://en.wikipedia.org/wiki/DPLL_algorithm.
|