Uses of Interface
net.sf.tweety.logics.commons.analysis.ConsistencyWitnessProvider

Packages that use ConsistencyWitnessProvider

Package	Description
net.sf.tweety.arg.adf.sat
net.sf.tweety.logics.pl.analysis
net.sf.tweety.logics.pl.sat

Uses of ConsistencyWitnessProvider in net.sf.tweety.arg.adf.sat

Classes in net.sf.tweety.arg.adf.sat that implement ConsistencyWitnessProvider

Modifier and Type	Class	Description
class	IncrementalSatSolver
class	NativeLingelingSolver	Experimental lingeling binding

Uses of ConsistencyWitnessProvider in net.sf.tweety.logics.pl.analysis

Fields in net.sf.tweety.logics.pl.analysis declared as ConsistencyWitnessProvider

Modifier and Type	Field	Description
private ConsistencyWitnessProvider<PlBeliefSet,PlFormula>	ContensionInconsistencyMeasurementProcess.witnessProvider	The witness provider used.
private ConsistencyWitnessProvider<PlBeliefSet,PlFormula>	HsInconsistencyMeasurementProcess.witnessProvider	The witness provider used.

Uses of ConsistencyWitnessProvider in net.sf.tweety.logics.pl.sat

Classes in net.sf.tweety.logics.pl.sat that implement ConsistencyWitnessProvider

Modifier and Type	Class	Description
class	LingelingSolver	A wrapper for the Lingeling SAT solver (tested with Lingeling version ats1 ce8c04fc97ef07cf279c0c5dcbbc7c5d9904230a).
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.