Uses of Interface
org.tweetyproject.logics.commons.analysis.BeliefSetConsistencyTester
Package
Description
-
Uses of BeliefSetConsistencyTester in org.tweetyproject.logics.commons.analysis
Modifier and TypeInterfaceDescriptioninterface
MusEnumerator<S extends Formula>
Interface for classes enumerating MUSes (minimal unsatisfiable sets) and MCSs (maximal consistent sets).Modifier and TypeClassDescriptionclass
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.ModifierConstructorDescriptionDrasticInconsistencyMeasure
(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
Modifier and TypeClassDescriptionclass
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 BeliefSetConsistencyTester in org.tweetyproject.logics.pl.sat
Modifier and TypeClassDescriptionclass
This class offers a generic wrapper for command line based SAT solvers.class
Generic class for Dimacs-based MaxSAT solvers.class
Interface for SAT solvers which work on the Dimacs format.class
Implements a MUs enumerator based on MARCO (http://sun.iwu.edu/~mliffito/marco/).class
Provides a generic class for implementing MaxSAT solvers, i.e.class
Implements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).class
Provides an interface to the open-wbo MaxSAT solver, see https://github.com/sat-group/open-wbo.class
This abstract class models a MUS enumerator for propositional logic, i.e.class
Uses the Sat4j library for SAT solving (note that currently only the light version is used).class
Abstract class for specifying SAT solvers.class
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 BeliefSetConsistencyTester in org.tweetyproject.logics.qbf.reasoner
Modifier and TypeClassDescriptionclass
A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver.class
A wrapper for the Caqe (https://www.react.uni-saarland.de/tools/caqe/ solver.class
A wrapper for the GhostQ (https://www.wklieber.com/ghostq/) solver.class
Abstract QBF sat solver to be implemented by concrete solvers.class
A wrapper for the Qute (https://www.ac.tuwien.ac.at/research/qute/) solver.