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.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
class	NativeMinisatSolver
class	NativePicosatSolver
class	SimpleIncrementalSatSolver	A simple wrapper which can be used where instances of IncrementalSatSolver are needed.

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	MaxSatSolver	Provides a generic class for implementing MaxSAT solvers, i.e.
class	OpenWboSolver	Provides an interface to the open-wbo MaxSAT solver, see https://github.com/sat-group/open-wbo.
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.