Uses of Interface
net.sf.tweety.logics.commons.analysis.ConsistencyTester
-
-
Uses of ConsistencyTester in net.sf.tweety.action.description.analysis
Subinterfaces of ConsistencyTester in net.sf.tweety.action.description.analysis Modifier and Type Interface Description interface
ActionDescriptionConsistencyTester<T extends CausalLaw>
Classes implementing this interface are capable of checking whether a given action description is consistent according to some consistency measurements.Classes in net.sf.tweety.action.description.analysis that implement ConsistencyTester Modifier and Type Class Description class
CActionDescriptionConsistencyTester
This class is able to check, whether a given action description in the action language C is consistent with regards to one simple consistency requirement: The transition system described by the action description has at least one state. -
Uses of ConsistencyTester in net.sf.tweety.arg.adf.sat
Classes in net.sf.tweety.arg.adf.sat that implement ConsistencyTester Modifier and Type Class Description class
IncrementalSatSolver
class
NativeLingelingSolver
Experimental lingeling bindingclass
NativeMinisatSolver
class
NativePicosatSolver
class
SimpleIncrementalSatSolver
A simple wrapper which can be used where instances ofIncrementalSatSolver
are needed. -
Uses of ConsistencyTester in net.sf.tweety.logics.commons.analysis
Subinterfaces of ConsistencyTester in net.sf.tweety.logics.commons.analysis Modifier and Type Interface Description interface
BeliefSetConsistencyTester<T extends Formula>
Classes extending this abstract class are capable of testing whether a given belief set is consistent.interface
MusEnumerator<S extends Formula>
Interface for classes enumerating MUSes (minimal unsatisfiable sets) and MCSs (maximal consistent sets).Classes in net.sf.tweety.logics.commons.analysis that implement ConsistencyTester Modifier and Type Class Description class
AbstractBeliefSetConsistencyTester<T 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. -
Uses of ConsistencyTester in net.sf.tweety.logics.pcl.analysis
Classes in net.sf.tweety.logics.pcl.analysis that implement ConsistencyTester Modifier and Type Class 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. -
Uses of ConsistencyTester in net.sf.tweety.logics.pl.sat
Classes in net.sf.tweety.logics.pl.sat that implement ConsistencyTester Modifier and Type Class 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
MaxSatSolver
Provides a generic class for implementing MaxSAT solvers, i.e.class
MimusMusEnumerator
Implements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).class
OpenWboSolver
Provides an interface to the open-wbo MaxSAT solver, see https://github.com/sat-group/open-wbo.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. -
Uses of ConsistencyTester in net.sf.tweety.logics.qbf.reasoner
Classes in net.sf.tweety.logics.qbf.reasoner that implement ConsistencyTester Modifier and Type Class Description class
CadetSolver
A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver.class
CaqeSolver
A wrapper for the Caqe (https://www.react.uni-saarland.de/tools/caqe/ solver.class
GhostQSolver
A wrapper for the GhostQ (https://www.wklieber.com/ghostq/) solver.class
QbfSolver
Abstract QBF sat solver to be implemented by concrete solvers.class
QuteSolver
A wrapper for the Qute (https://www.ac.tuwien.ac.at/research/qute/) solver.
-