Uses of Interface
org.sat4j.specs.ISolver

Packages that use ISolver

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.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.reader	Some utility classes to read problems from plain text files.
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

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

protected ISolver

AbstractLauncher.solver

Methods in org.sat4j with type parameters of type ISolver

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

protected ISolver	MUSLauncher.configureSolver(String[] args)
protected ISolver	BasicLauncher.configureSolver(String[] args)
protected abstract ISolver	AbstractLauncher.configureSolver(String[] args)
ISolver	LightFactory.defaultSolver()
ISolver	LightFactory.lightSolver()

Methods in org.sat4j with parameters of type ISolver

protected Reader	MUSLauncher.createReader(ISolver theSolver, String problemname)
protected Reader	BasicLauncher.createReader(ISolver theSolver, String problemname)
protected abstract Reader	AbstractLauncher.createReader(ISolver theSolver, String problemname)

Uses of ISolver in org.sat4j.core

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

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

void	ConstrGroup.removeFrom(ISolver solver)

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.
static ISolver	SolverFactory.newMinOneSolver()

Uses of ISolver in org.sat4j.minisat.core

Subinterfaces of ISolver in org.sat4j.minisat.core

interface

ICDCL<D extends DataStructureFactory> Abstraction for Conflict Driven Clause Learning Solver.

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

class

Solver<D extends DataStructureFactory> 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 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

AbstractSelectorVariablesDecorator(ISolver solver)

MaxSatDecorator(ISolver solver)

MaxSatDecorator(ISolver solver, boolean equivalence)

MinOneDecorator(ISolver solver)

Uses of ISolver in org.sat4j.reader

Fields in org.sat4j.reader declared as ISolver

protected ISolver

DimacsReader.solver

Methods in org.sat4j.reader that return ISolver

protected ISolver

DimacsReader.getSolver()

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

DimacsReader(ISolver solver)

DimacsReader(ISolver solver, String format)

InstanceReader(ISolver solver)

LecteurDimacs(ISolver s)

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

GroupedCNFReader(HighLevelXplain<ISolver> solver)

Uses of ISolver in org.sat4j.tools

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

class	ClausalCardinalitiesDecorator<T extends ISolver> A decorator for clausal cardinalities constraints.
class	LexicoDecorator<T extends ISolver>
class	ManyCore<S extends ISolver> A class allowing to run several solvers in parallel.
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

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	GateTranslator Utility class to easily feed a SAT solver using logical gates.
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	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.

Fields in org.sat4j.tools declared as ISolver

protected ISolver

DimacsArrayReader.solver

Methods in org.sat4j.tools that return ISolver

protected ISolver	DimacsArrayReader.getSolver()
ISolver	DimacsArrayReader.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)

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)

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)

Minimal4InclusionModel(ISolver solver)

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.

SingleSolutionDetector(ISolver solver)

SolutionCounter(ISolver solver)

Uses of ISolver in org.sat4j.tools.encoding

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

IConstr	Product.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	Policy.addAtLeast(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	Binomial.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Binomial.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	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
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	Product.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	Commander.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Commander.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binomial.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binary.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

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

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

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	InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	DeletionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)