Uses of Interface
org.sat4j.specs.RandomAccessModel

Packages that use RandomAccessModel

Package	Description
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
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.xplain	Implementation of an explanation engine in case of unsatisfiability.

Uses of RandomAccessModel in org.sat4j.minisat.core

Subinterfaces of RandomAccessModel 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 RandomAccessModel

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.

Uses of RandomAccessModel in org.sat4j.opt

Classes in org.sat4j.opt that implement RandomAccessModel

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.

Uses of RandomAccessModel in org.sat4j.specs

Subinterfaces of RandomAccessModel in org.sat4j.specs

Modifier and Type	Interface and Description
interface	IGroupSolver Represents a CNF in which clauses are grouped into levels.
interface	IOptimizationProblem Represents an optimization problem.
interface	IProblem Access to the information related to a given problem instance.
interface	ISolver This interface contains all services provided by a SAT solver.

Methods in org.sat4j.specs with parameters of type RandomAccessModel

Modifier and Type	Method and Description
void	SearchListener.solutionFound(int[] model, RandomAccessModel lazyModel) a solution is found.

Uses of RandomAccessModel in org.sat4j.tools

Classes in org.sat4j.tools that implement RandomAccessModel

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

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

Modifier and Type	Method and Description
void	TextOutputTracing.solutionFound(int[] model, RandomAccessModel lazyModel)
void	DotSearchTracing.solutionFound(int[] model, RandomAccessModel lazyModel)
void	SearchListenerAdapter.solutionFound(int[] model, RandomAccessModel lazyModel)
void	SearchEnumeratorListener.solutionFound(int[] model, RandomAccessModel lazyModel)
void	SearchMinOneListener.solutionFound(int[] model, RandomAccessModel lazyModel)
void	LearnedTracing.solutionFound(int[] model, RandomAccessModel lazyModel)
void	HeuristicsTracing.solutionFound(int[] model, RandomAccessModel lazyModel)
void	MultiTracing.solutionFound(int[] model, RandomAccessModel lazyModel)

Uses of RandomAccessModel in org.sat4j.tools.xplain

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

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.