Uses of Interface
org.sat4j.specs.ISolver

Packages that use ISolver

Package	Description
org.sat4j	Contains a command line launcher for the SAT solvers.
org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
org.sat4j.csp	Classes needed for CSP to SAT translation.
org.sat4j.csp.constraints	Classes needed for CSP to SAT translation.
org.sat4j.csp.encodings
org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.pb	Implementations of pseudo boolean solvers
org.sat4j.pb.core	Implementations of pseudo boolean solvers
org.sat4j.pb.tools	Implementation of different tools for pseudo boolean solvers
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.sat	Implementation of a sat4j Launcher.
org.sat4j.specs	Those classes are intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.encoding	Implementation of different encodings.
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

Uses of ISolver in org.sat4j

Classes in org.sat4j with type parameters of type ISolver

Modifier and Type	Class and Description
class	BasicLauncher<T extends ISolver> Very simple launcher, to be used during the SAT competition or the SAT race for instance.

Fields in org.sat4j declared as ISolver

Modifier and Type	Field and Description
protected ISolver	AbstractLauncher.solver

Methods in org.sat4j with type parameters of type ISolver

Modifier and Type	Method and Description
protected <T extends ISolver> void	AbstractLauncher.showAvailableSolvers(ASolverFactory<T> afactory)
protected <T extends ISolver> void	AbstractLauncher.showAvailableSolvers(ASolverFactory<T> afactory, String framework)

Methods in org.sat4j that return ISolver

Modifier and Type	Method and Description
protected abstract ISolver	AbstractLauncher.configureSolver(String[] args)
protected ISolver	BasicLauncher.configureSolver(String[] args)
protected ISolver	MUSLauncher.configureSolver(String[] args)
ISolver	LightFactory.defaultSolver()
ISolver	LightFactory.lightSolver()

Methods in org.sat4j with parameters of type ISolver

Modifier and Type	Method and Description
protected abstract Reader	AbstractLauncher.createReader(ISolver theSolver, String problemname)
protected Reader	BasicLauncher.createReader(ISolver theSolver, String problemname)
protected Reader	MUSLauncher.createReader(ISolver theSolver, String problemname)
void	ILauncherMode.displayResult(ISolver solver, IProblem problem, ILogAble logger, PrintWriter out, Reader reader, long beginTime, boolean displaySolutionLine) Output of the launcher when the solver stops

Uses of ISolver in org.sat4j.core

Classes in org.sat4j.core with type parameters of type ISolver

Modifier and Type	Class and Description
class	ASolverFactory<T extends ISolver> A solver factory is responsible for providing prebuilt solvers to the end user.

Methods in org.sat4j.core with parameters of type ISolver

Modifier and Type	Method and Description
void	ConstrGroup.removeFrom(ISolver solver)

Uses of ISolver in org.sat4j.csp

Methods in org.sat4j.csp that return ISolver

Modifier and Type	Method and Description
protected ISolver	CSPLauncher.configureSolver(String[] args)
ISolver	SolverFactory.defaultSolver()
ISolver	SolverFactory.lightSolver()
static ISolver	SolverFactory.newCuttingPlanes()
static ISolver	SolverFactory.newDefault() Default solver of the SolverFactory.
static ISolver	SolverFactory.newDimacsOutput()
static ISolver	SolverFactory.newLight() Small footprint SAT solver.
static ISolver	SolverFactory.newSAT()
static ISolver	SolverFactory.newUNSAT()

Methods in org.sat4j.csp with parameters of type ISolver

Modifier and Type	Method and Description
protected Reader	CSPLauncher.createReader(ISolver aSolver, String problemname)
void	Encoding.onFinish(ISolver solver, IVec<Var> scope)
void	Encoding.onInit(ISolver solver, IVec<Var> scope)
void	Encoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	Encoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	Var.toClause(ISolver solver)
void	Constant.toClause(ISolver solver)
void	Evaluable.toClause(ISolver solver) Translates a variable over a domain into a set a clauses enforcing that exactly one value must be chosen in the domain.
void	Predicate.toClause(ISolver solver, IVec<Var> vscope, IVec<Evaluable> vars)
void	Clausifiable.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)

Uses of ISolver in org.sat4j.csp.constraints

Methods in org.sat4j.csp.constraints with parameters of type ISolver

Modifier and Type	Method and Description
void	Nogoods.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	AllDiff.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	AllDiffCard.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	Supports.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)

Uses of ISolver in org.sat4j.csp.encodings

Methods in org.sat4j.csp.encodings with parameters of type ISolver

Modifier and Type	Method and Description
void	GeneralizedSupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	BinarySupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	DirectEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	GeneralizedSupportEncoding.onInit(ISolver solver, IVec<Var> scope)
void	BinarySupportEncoding.onInit(ISolver solver, IVec<Var> scope)
void	DirectEncoding.onInit(ISolver solver, IVec<Var> scope)
void	GeneralizedSupportEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	BinarySupportEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	DirectEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	GeneralizedSupportEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	BinarySupportEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
void	DirectEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)

Uses of ISolver in org.sat4j.maxsat

Classes in org.sat4j.maxsat that implement ISolver

Modifier and Type	Class and Description
class	MinCostDecorator A decorator that computes minimal cost models.
class	WeightedMaxSatDecorator A decorator for solving weighted MAX SAT problems.

Methods in org.sat4j.maxsat that return ISolver

Modifier and Type	Method and Description
protected ISolver	GenericOptLauncher.configureSolver(String[] args)

Methods in org.sat4j.maxsat with parameters of type ISolver

Modifier and Type	Method and Description
protected Reader	GenericOptLauncher.createReader(ISolver aSolver, String problemname)

Uses of ISolver in org.sat4j.minisat

Methods in org.sat4j.minisat that return ISolver

Modifier and Type	Method and Description
ISolver	SolverFactory.defaultSolver()
ISolver	SolverFactory.lightSolver()
static ISolver	SolverFactory.newDefault() Default solver of the SolverFactory.
static ISolver	SolverFactory.newDimacsOutput()
static ISolver	SolverFactory.newLight() Small footprint SAT solver.
static ISolver	SolverFactory.newMinOneSolver()
static ISolver	SolverFactory.newParallel()
static ISolver	SolverFactory.newSATUNSAT() Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
static ISolver	SolverFactory.newStatistics()

Uses of ISolver in org.sat4j.minisat.core

Subinterfaces of ISolver in org.sat4j.minisat.core

Modifier and Type	Interface and Description
interface	ICDCL<D extends DataStructureFactory> Abstraction for Conflict Driven Clause Learning Solver.

Classes in org.sat4j.minisat.core that implement ISolver

Modifier and Type	Class and Description
class	Solver<D extends DataStructureFactory> The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Methods in org.sat4j.minisat.core that return ISolver

Modifier and Type	Method and Description
ISolver	Solver.getSolvingEngine()

Uses of ISolver in org.sat4j.opt

Classes in org.sat4j.opt that implement ISolver

Modifier and Type	Class and Description
class	AbstractSelectorVariablesDecorator Abstract class which adds a new "selector" variable for each clause entered in the solver.
class	MaxSatDecorator Computes a solution that satisfies the maximum of clauses.
class	MinOneDecorator Computes a solution with the smallest number of satisfied literals.

Constructors in org.sat4j.opt with parameters of type ISolver

Constructor and Description
AbstractSelectorVariablesDecorator(ISolver solver)
MaxSatDecorator(ISolver solver)
MaxSatDecorator(ISolver solver, boolean equivalence)
MinOneDecorator(ISolver solver)

Uses of ISolver in org.sat4j.pb

Subinterfaces of ISolver in org.sat4j.pb

Modifier and Type	Interface and Description
interface	IPBSolver A solver able to deal with pseudo boolean constraints.

Classes in org.sat4j.pb that implement ISolver

Modifier and Type	Class and Description
class	ConstraintRelaxingPseudoOptDecorator
class	LPStringSolver Solver used to display in a string the pb-instance in OPB format.
class	OPBStringSolver Solver used to display in a string the pb-instance in OPB format.
class	OptToPBSATAdapter Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.
class	PBSolverDecorator A decorator for the PB solvers.
class	PseudoBitsAdderDecorator A decorator that computes minimal pseudo boolean models.
class	PseudoIteratorDecorator A decorator that computes all pseudo boolean models.
class	PseudoOptDecorator A decorator that computes minimal pseudo boolean models.
class	UserFriendlyPBStringSolver<T> Solver to display SAT instances using domain objects names instead of Dimacs numbers.

Methods in org.sat4j.pb that return ISolver

Modifier and Type	Method and Description
protected ISolver	LanceurPseudo2007Eclipse.configureSolver(String[] args)
protected ISolver	LanceurPseudo2005.configureSolver(String[] args)

Methods in org.sat4j.pb with parameters of type ISolver

Modifier and Type	Method and Description
BigInteger	ObjectiveFunction.calculateDegreeImplicant(ISolver solver) Compute the degree of the objective function using a prime implicant.
protected Reader	LanceurPseudo2007Eclipse.createReader(ISolver theSolver, String problemname)
protected Reader	LanceurPseudo2005.createReader(ISolver theSolver, String problemname)
protected Reader	LanceurPseudo2007.createReader(ISolver theSolver, String problemname)

Uses of ISolver in org.sat4j.pb.core

Subinterfaces of ISolver in org.sat4j.pb.core

Modifier and Type	Interface and Description
interface	IPBCDCLSolver<D extends PBDataStructureFactory> Abstraction for Conflict Driven Clause Learning PBSolver.

Classes in org.sat4j.pb.core that implement ISolver

Modifier and Type	Class and Description
class	ObjectiveReducerPBSolverDecorator
class	PBSolver
class	PBSolverCautious
class	PBSolverClause
class	PBSolverCP
class	PBSolverResCP
class	PBSolverResolution
class	PBSolverWithImpliedClause

Methods in org.sat4j.pb.core that return ISolver

Modifier and Type	Method and Description
ISolver	ObjectiveReducerPBSolverDecorator.getSolvingEngine()

Uses of ISolver in org.sat4j.pb.tools

Classes in org.sat4j.pb.tools that implement ISolver

Modifier and Type	Class and Description
class	ClausalConstraintsDecorator
class	LexicoDecoratorPB
class	ManyCorePB
class	PBAdapter Allow to put a ISolver when an IPBSolver is required.
class	SteppedTimeoutLexicoDecoratorPB
class	XplainPB

Constructors in org.sat4j.pb.tools with parameters of type ISolver

Constructor and Description
PBAdapter(ISolver solver)

Uses of ISolver in org.sat4j.reader

Classes in org.sat4j.reader with type parameters of type ISolver

Modifier and Type	Class and Description
class	JSONReader<S extends ISolver> Simple JSON reader for clauses and cardinality constraints.

Fields in org.sat4j.reader declared as ISolver

Modifier and Type	Field and Description
protected S	JSONReader.solver
protected ISolver	DimacsReader.solver

Methods in org.sat4j.reader that return ISolver

Modifier and Type	Method and Description
protected ISolver	DimacsReader.getSolver()
ISolver	JSONReader.parseString(String json)

Constructors in org.sat4j.reader with parameters of type ISolver

Constructor and Description
CSPExtSupportReader(ISolver solver, boolean allDiffCard)
CSPInstanceReader(ISolver solver, boolean allDiffCard)
CSPReader(ISolver solver, boolean allDiffCard)
CSPSupportReader(ISolver solver, boolean allDiffCard)
DimacsReader(ISolver solver)
DimacsReader(ISolver solver, String format)
InstanceReader(ISolver solver)
LecteurDimacs(ISolver s)
XMLCSPReader(ISolver solver, boolean allDiffCard)

Uses of ISolver in org.sat4j.sat

Methods in org.sat4j.sat with type parameters of type ISolver

Modifier and Type	Method and Description
static <T extends ISolver> void	Solvers.showAvailableSolvers(ASolverFactory<T> afactory, ILogAble logger)
static <T extends ISolver> void	Solvers.showAvailableSolvers(ASolverFactory<T> afactory, String framework, ILogAble logger)

Methods in org.sat4j.sat that return ISolver

Modifier and Type	Method and Description
protected ISolver	Launcher.configureSolver(String[] args) Configure the solver according to the command line parameters.
ISolver	DetailedCommandPanel.getSolver()

Methods in org.sat4j.sat with parameters of type ISolver

Modifier and Type	Method and Description
protected Reader	DetailedCommandPanel.createReader(ISolver theSolver, String problemname)
protected Reader	Launcher.createReader(ISolver theSolver, String problemname)
protected Reader	Lanceur.createReader(ISolver theSolver, String problemname) Deprecated.

Uses of ISolver in org.sat4j.specs

Subinterfaces of ISolver in org.sat4j.specs

Modifier and Type	Interface and Description
interface	IGroupSolver Represents a CNF in which clauses are grouped into levels.

Methods in org.sat4j.specs that return ISolver

Modifier and Type	Method and Description
ISolver	ISolver.getSolvingEngine() Retrieve the real engine in case the engine is decorated by one or several decorator.

Uses of ISolver in org.sat4j.tools

Classes in org.sat4j.tools with type parameters of type ISolver

Modifier and Type	Class and Description
class	AbstractClauseSelectorSolver<T extends ISolver>
class	ClausalCardinalitiesDecorator<T extends ISolver> A decorator for clausal cardinalities constraints.
class	FullClauseSelectorSolver<T extends ISolver>
class	GroupClauseSelectorSolver<T extends ISolver>
class	LexicoDecorator<T extends ISolver>
class	ManyCore<S extends ISolver> A class allowing to run several solvers in parallel.
class	NegationDecorator<T extends ISolver> Negates the formula inside a solver.
class	SolverDecorator<T extends ISolver> The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.

Classes in org.sat4j.tools that implement ISolver

Modifier and Type	Class and Description
class	AbstractClauseSelectorSolver<T extends ISolver>
class	AbstractMinimalModel
class	AbstractOutputSolver
class	ClausalCardinalitiesDecorator<T extends ISolver> A decorator for clausal cardinalities constraints.
class	DimacsOutputSolver Solver used to display in a writer the CNF instance in Dimacs format.
class	DimacsStringSolver Solver used to write down a CNF into a String.
class	FullClauseSelectorSolver<T extends ISolver>
class	GateTranslator Utility class to easily feed a SAT solver using logical gates.
class	GroupClauseSelectorSolver<T extends ISolver>
class	LexicoDecorator<T extends ISolver>
class	ManyCore<S extends ISolver> A class allowing to run several solvers in parallel.
class	Minimal4CardinalityModel Computes models with a minimal number (with respect to cardinality) of negative literals.
class	Minimal4InclusionModel Computes models with a minimal subset (with respect to set inclusion) of negative literals.
class	ModelIterator That class allows to iterate through all the models (implicants) of a formula.
class	ModelIteratorToSATAdapter This class allow to use the ModelIterator class as a solver.
class	NegationDecorator<T extends ISolver> Negates the formula inside a solver.
class	OptToSatAdapter
class	SingleSolutionDetector This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not.
class	SolutionCounter Another solver decorator that counts the number of solutions.
class	SolverDecorator<T extends ISolver> The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.
class	StatisticsSolver

Fields in org.sat4j.tools declared as ISolver

Modifier and Type	Field and Description
protected ISolver	DimacsArrayReader.solver

Methods in org.sat4j.tools with type parameters of type ISolver

Modifier and Type	Method and Description
<T extends ISolver> T	AllMUSes.getSolverInstance() Gets an instance of ISolver that can be used to compute all MUSes

Methods in org.sat4j.tools that return ISolver

Modifier and Type	Method and Description
protected ISolver	DimacsArrayReader.getSolver()
ISolver	AbstractOutputSolver.getSolvingEngine()
ISolver	ManyCore.getSolvingEngine()
ISolver	StatisticsSolver.getSolvingEngine()
ISolver	SolverDecorator.getSolvingEngine()
ISolver	DimacsArrayReader.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)

Methods in org.sat4j.tools with parameters of type ISolver

Modifier and Type	Method and Description
static IVecInt	RemiUtils.backbone(ISolver s) Compute the set of literals common to all models of the formula.
static IVecInt	Backbone.compute(ISolver solver) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
static IVecInt	Backbone.compute(ISolver solver, int[] implicant)
static IVecInt	Backbone.compute(ISolver solver, int[] implicant, IVecInt assumptions)
static IVecInt	Backbone.compute(ISolver solver, IVecInt assumptions) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
static IVecInt	AbstractMinimalModel.negativeLiterals(ISolver solver)
static IVecInt	AbstractMinimalModel.positiveLiterals(ISolver solver)

Constructors in org.sat4j.tools with parameters of type ISolver

Constructor and Description
AbstractMinimalModel(ISolver solver)
AbstractMinimalModel(ISolver solver, IVecInt p)
AbstractMinimalModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
AbstractMinimalModel(ISolver solver, SolutionFoundListener modelListener)
DimacsArrayReader(ISolver solver)
ExtendedDimacsArrayReader(ISolver solver)
GateTranslator(ISolver solver)
ManyCore(S... solverObjects)
ManyCore(String[] names, S... solverObjects) Create a parallel solver from a list of solvers and a list of names.
Minimal4CardinalityModel(ISolver solver)
Minimal4CardinalityModel(ISolver solver, IVecInt p)
Minimal4CardinalityModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
Minimal4CardinalityModel(ISolver solver, SolutionFoundListener modelListener)
Minimal4InclusionModel(ISolver solver)
Minimal4InclusionModel(ISolver solver, IVecInt p)
Minimal4InclusionModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
ModelIterator(ISolver solver) Create an iterator over the solutions available in solver.
ModelIterator(ISolver solver, long bound) Create an iterator over a limited number of solutions available in solver.
ModelIteratorToSATAdapter(ISolver solver, long bound, SolutionFoundListener sfl)
ModelIteratorToSATAdapter(ISolver solver, SolutionFoundListener sfl)
SingleSolutionDetector(ISolver solver)
SolutionCounter(ISolver solver)

Constructor parameters in org.sat4j.tools with type arguments of type ISolver

Constructor and Description
AllMUSes(ASolverFactory<? extends ISolver> factory)
AllMUSes(boolean group, ASolverFactory<? extends ISolver> factory)
CheckMUSSolutionListener(ASolverFactory<? extends ISolver> factory)

Uses of ISolver in org.sat4j.tools.encoding

Methods in org.sat4j.tools.encoding with parameters of type ISolver

Modifier and Type	Method and Description
IConstr	Policy.addAtLeast(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addAtMost(ISolver solver, IVecInt literals, int k) This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Sequential.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binary.addAtMostOne(ISolver solver, IVecInt literals) p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Sequential.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Product.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Commander.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binary.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binomial.addExactlyOne(ISolver solver, IVecInt literals)

Uses of ISolver in org.sat4j.tools.xplain

Classes in org.sat4j.tools.xplain with type parameters of type ISolver

Modifier and Type	Class and Description
class	HighLevelXplain<T extends ISolver> Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.
class	Xplain<T extends ISolver> Explanation framework for SAT4J.

Classes in org.sat4j.tools.xplain that implement ISolver

Modifier and Type	Class and Description
class	HighLevelXplain<T extends ISolver> Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.
class	Xplain<T extends ISolver> Explanation framework for SAT4J.

Methods in org.sat4j.tools.xplain with parameters of type ISolver

Modifier and Type	Method and Description
IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	QuickXplain2001Strategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	MinimizationStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	DeletionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)