Uses of Interface
org.sat4j.specs.ISolver

Packages that use ISolver

org.sat4j	Contain a command line launcher for the SAT solvers.
org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.reader.csp	Classes needed for CSP to SAT translation.
org.sat4j.tools	Tools to be used on top of an ISolver.

Uses of ISolver in org.sat4j

Fields in org.sat4j declared as ISolver

protected ISolver

AbstractLauncher.solver

Methods in org.sat4j that return ISolver

protected ISolver	GenericOptLauncher.configureSolver(java.lang.String[] args)
protected ISolver	LanceurPseudo2005.configureSolver(java.lang.String[] args)
protected ISolver	MaxSatLauncher.configureSolver(java.lang.String[] args)
protected ISolver	Lanceur.configureSolver(java.lang.String[] args) Configure the solver according to the command line parameters.
protected ISolver	CSPLauncher.configureSolver(java.lang.String[] args)
protected abstract ISolver	AbstractLauncher.configureSolver(java.lang.String[] args)

Methods in org.sat4j with parameters of type ISolver

protected Reader	LanceurPseudo2007.createReader(ISolver solver, java.lang.String problemname)
protected Reader	GenericOptLauncher.createReader(ISolver solver, java.lang.String problemname)
protected Reader	LanceurPseudo2005.createReader(ISolver solver, java.lang.String problemname)
protected Reader	MaxSatLauncher.createReader(ISolver solver, java.lang.String problemname)
protected Reader	Lanceur.createReader(ISolver solver, java.lang.String problemname)
protected Reader	CSPLauncher.createReader(ISolver solver, java.lang.String problemname)
protected abstract Reader	AbstractLauncher.createReader(ISolver solver, java.lang.String problemname)

Uses of ISolver in org.sat4j.core

Methods in org.sat4j.core that return ISolver

ISolver	ASolverFactory.createSolverByName(java.lang.String solvername) create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.
abstract ISolver	ASolverFactory.defaultSolver() To obtain the default solver of the library.
abstract ISolver	ASolverFactory.lightSolver() To obtain a solver that is suitable for solving many small instances of SAT problems.

Uses of ISolver in org.sat4j.minisat

Methods in org.sat4j.minisat that return ISolver

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.

Uses of ISolver in org.sat4j.minisat.constraints.pb

Classes in org.sat4j.minisat.constraints.pb that implement ISolver

class	PBSolver<L extends ILits>
class	PBSolverClause
class	PBSolverMerging
class	PBSolverWithImpliedClause

Uses of ISolver in org.sat4j.minisat.core

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

class

Solver<L extends ILits> The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Uses of ISolver in org.sat4j.opt

Classes in org.sat4j.opt that implement ISolver

class	AbstractSelectorVariablesDecorator
class	MaxSatDecorator
class	MinCostDecorator A decorator that computes minimal cost models.
class	MinOneDecorator Computes a solution with the smallest number of satisfied literals.
class	PseudoOptDecorator A decorator that computes minimal pseudo boolean models.
class	WeightedMaxSatDecorator

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

AbstractSelectorVariablesDecorator(ISolver solver)

MaxSatDecorator(ISolver solver)

MinCostDecorator(ISolver solver)

MinOneDecorator(ISolver solver)

PseudoOptDecorator(ISolver solver)

WeightedMaxSatDecorator(ISolver solver)

Uses of ISolver in org.sat4j.reader

Fields in org.sat4j.reader declared as ISolver

protected ISolver	DimacsReader.solver
protected ISolver	OPBReader2005.solver

Methods in org.sat4j.reader that return ISolver

protected ISolver

DimacsReader.getSolver()

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

CardDimacsReader(ISolver solver)
Deprecated.

CSPExtSupportReader(ISolver solver)

CSPReader(ISolver solver)

CSPSupportReader(ISolver solver)

DimacsReader(ISolver solver)

DimacsReader(ISolver solver, java.lang.String format)

ExtendedDimacsReader(ISolver solver)

GoodOPBReader(ISolver solver)

InstanceReader(ISolver solver)

LecteurDimacs(ISolver s)

OPBReader2005(ISolver solver)

OPBReader2006(ISolver solver)

OPBReader2007(ISolver solver)

XMLCSPReader(ISolver solver)

Uses of ISolver in org.sat4j.reader.csp

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

void	GeneralizedSupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	DirectEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	BinarySupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	Encoding.onFinish(ISolver solver, IVec<Var> scope)
void	GeneralizedSupportEncoding.onInit(ISolver solver, IVec<Var> scope)
void	DirectEncoding.onInit(ISolver solver, IVec<Var> scope)
void	BinarySupportEncoding.onInit(ISolver solver, IVec<Var> scope)
void	Encoding.onInit(ISolver solver, IVec<Var> scope)
void	GeneralizedSupportEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	DirectEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	BinarySupportEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	Encoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	GeneralizedSupportEncoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	DirectEncoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	BinarySupportEncoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	Encoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
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	Var.toClause(ISolver solver)
void	AllDiff.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	Nogoods.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	Supports.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
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.tools

Classes in org.sat4j.tools that implement ISolver

class	DimacsOutputSolver Solver used to display in a writer the CNF instance in Dimacs format.
class	GateTranslator Utility class to easily feed a SAT solver using logical gates.
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	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 The aim of that class is to allow adding dynamic responsabilities to SAT solvers using the Decorator design pattern.

Fields in org.sat4j.tools declared as ISolver

protected ISolver

DimacsArrayReader.solver

Methods in org.sat4j.tools that return ISolver

ISolver	SolverDecorator.decorated()
protected ISolver	DimacsArrayReader.getSolver()

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

static IVecInt

RemiUtils.backbone(ISolver s) Compute the set of literals common to all models of the formula.

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

DimacsArrayReader(ISolver solver)

ExtendedDimacsArrayReader(ISolver solver)

GateTranslator(ISolver solver)

Minimal4CardinalityModel(ISolver solver)

Minimal4InclusionModel(ISolver solver)

ModelIterator(ISolver solver)

SingleSolutionDetector(ISolver solver)

SolutionCounter(ISolver solver)

SolverDecorator(ISolver solver)