Uses of Interface
org.tweetyproject.logics.commons.analysis.BeliefSetConsistencyTester
Packages that use BeliefSetConsistencyTester
Package
Description
-
Uses of BeliefSetConsistencyTester in org.tweetyproject.logics.commons.analysis
Subinterfaces of BeliefSetConsistencyTester in org.tweetyproject.logics.commons.analysisModifier and TypeInterfaceDescriptioninterfaceMusEnumerator<S extends Formula>Interface for classes enumerating MUSes (minimal unsatisfiable sets) and MCSs (maximal consistent sets).Classes in org.tweetyproject.logics.commons.analysis that implement BeliefSetConsistencyTesterModifier and TypeClassDescriptionclassAbstractBeliefSetConsistencyTester<T extends Formula>Classes extending this abstract class are capable of testing whether a given belief set is consistent.classAbstractMusEnumerator<S extends Formula>Abstract implementation for MUes enumerators.classNaiveMusEnumerator<S extends Formula>A simple approach to compute minimal inconsistent subsets and maximal consistent subsets by exhaustive search.Constructors in org.tweetyproject.logics.commons.analysis with parameters of type BeliefSetConsistencyTesterModifierConstructorDescriptionDrasticInconsistencyMeasure(BeliefSetConsistencyTester<S> consTester) Creates a new drastic inconsistency measure.Creates a new naive MusEnumerator that uses the given consistency tester. -
Uses of BeliefSetConsistencyTester in org.tweetyproject.logics.pcl.analysis
Classes in org.tweetyproject.logics.pcl.analysis that implement BeliefSetConsistencyTesterModifier and TypeClassDescriptionclassThis 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 BeliefSetConsistencyTester in org.tweetyproject.logics.pl.sat
Classes in org.tweetyproject.logics.pl.sat that implement BeliefSetConsistencyTesterModifier and TypeClassDescriptionclassThis class offers a generic wrapper for command line based SAT solvers.classImplements a MUs enumerator based on MARCO (http://sun.iwu.edu/~mliffito/marco/).classProvides a generic class for implementing MaxSAT solvers, i.e.classImplements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).classProvides an interface to the open-wbo MaxSAT solver, see https://github.com/sat-group/open-wbo.classThis abstract class models a MUS enumerator for propositional logic, i.e.classUses the Sat4j library for SAT solving (note that currently only the light version is used).classAbstract class for specifying SAT solvers.classThis 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 BeliefSetConsistencyTester in org.tweetyproject.logics.qbf.reasoner
Classes in org.tweetyproject.logics.qbf.reasoner that implement BeliefSetConsistencyTesterModifier and TypeClassDescriptionclassA wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver.classA wrapper for the Caqe (https://www.react.uni-saarland.de/tools/caqe/ solver.classA wrapper for the GhostQ (https://www.wklieber.com/ghostq/) solver.classAbstract QBF sat solver to be implemented by concrete solvers.classA wrapper for the Qute (https://www.ac.tuwien.ac.at/research/qute/) solver.