Uses of Class
net.sf.tweety.logics.pl.sat.SatSolver

Packages that use SatSolver

Package	Description
net.sf.tweety.arg.adf.sat
net.sf.tweety.arg.adf.semantics
net.sf.tweety.arg.dung.reasoner
net.sf.tweety.logics.pl.sat
net.sf.tweety.web.services

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

Subclasses of SatSolver in net.sf.tweety.arg.adf.sat

Modifier and Type	Class	Description
class	IncrementalSatSolver
class	NativeLingelingSolver	Experimental lingeling binding
class	SimpleIncrementalSatSolver	A simple wrapper which can be used where instances of IncrementalSatSolver are needed.

Fields in net.sf.tweety.arg.adf.sat declared as SatSolver

Modifier and Type	Field	Description
private SatSolver	SimpleIncrementalSatSolver.delegate
private SatSolver	SimpleSatSolverState.solver

Constructors in net.sf.tweety.arg.adf.sat with parameters of type SatSolver

Constructor	Description
SimpleIncrementalSatSolver(SatSolver delegate)
SimpleSatSolverState(SatSolver solver)

Uses of SatSolver in net.sf.tweety.arg.adf.semantics

Fields in net.sf.tweety.arg.adf.semantics declared as SatSolver

Modifier and Type	Field	Description
private SatSolver	SatLinkStrategy.solver

Constructors in net.sf.tweety.arg.adf.semantics with parameters of type SatSolver

Constructor	Description
SatLinkStrategy(SatSolver solver)

Uses of SatSolver in net.sf.tweety.arg.dung.reasoner

Fields in net.sf.tweety.arg.dung.reasoner declared as SatSolver

Modifier and Type	Field	Description
private SatSolver	SeeAcceptabilityReasoner.satSolver
protected SatSolver	AbstractSatExtensionReasoner.solver	A SAT solver

Constructors in net.sf.tweety.arg.dung.reasoner with parameters of type SatSolver

Constructor	Description
AbstractSatExtensionReasoner(SatSolver solver)	Instantiates a new reasoner that uses the given SAT solver
SatCompleteReasoner(SatSolver solver)	Constructs a new complete reasoner.
SatStableReasoner(SatSolver solver)	Constructs a new stable reasoner.
SeeAcceptabilityReasoner(SatSolver satSolver)	Creates a new IaqAcceptabilityReasoner.

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

Subclasses of SatSolver in net.sf.tweety.logics.pl.sat

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	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.

Fields in net.sf.tweety.logics.pl.sat declared as SatSolver

Modifier and Type	Field	Description
private static SatSolver	SatSolver.defaultSatSolver	The default SAT solver.

Methods in net.sf.tweety.logics.pl.sat that return SatSolver

Modifier and Type	Method	Description
static SatSolver	SatSolver.getDefaultSolver()	Returns the default SAT solver. If a default SAT solver has been configured this solver is returned by this method.

Methods in net.sf.tweety.logics.pl.sat with parameters of type SatSolver

Modifier and Type	Method	Description
static void	SatSolver.setDefaultSolver(SatSolver solver)	Sets the default SAT solver.

Uses of SatSolver in net.sf.tweety.web.services

Fields in net.sf.tweety.web.services declared as SatSolver

Modifier and Type	Field	Description
static SatSolver	InconsistencyMeasurementService.satSolver	The SAT solver configured for this service.