|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use IProblem | |
---|---|
org.sat4j | Contains a command line launcher for the SAT solvers. |
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.specs | Those classes are intented for users dealing with SAT solvers as blackboxes. |
org.sat4j.tools | Tools to be used on top of an ISolver. |
Uses of IProblem in org.sat4j |
---|
Methods in org.sat4j that return IProblem | |
---|---|
protected IProblem |
AbstractLauncher.readProblem(java.lang.String problemname)
Reads a problem file from the command line. |
Methods in org.sat4j with parameters of type IProblem | |
---|---|
protected void |
AbstractLauncher.solve(IProblem problem)
|
protected void |
AbstractOptimizationLauncher.solve(IProblem problem)
|
Uses of IProblem in org.sat4j.minisat.core |
---|
Classes in org.sat4j.minisat.core that implement IProblem | |
---|---|
class |
Solver<L extends ILits,D extends DataStructureFactory<L>>
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver. |
Uses of IProblem in org.sat4j.opt |
---|
Classes in org.sat4j.opt that implement IProblem | |
---|---|
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 IProblem in org.sat4j.reader |
---|
Methods in org.sat4j.reader that return IProblem | |
---|---|
IProblem |
LecteurDimacs.parseInstance(java.io.InputStream input)
|
IProblem |
Reader.parseInstance(java.io.InputStream in)
|
IProblem |
AIGReader.parseInstance(java.io.InputStream in)
|
IProblem |
AAGReader.parseInstance(java.io.Reader in)
|
IProblem |
InstanceReader.parseInstance(java.io.Reader in)
|
IProblem |
DimacsReader.parseInstance(java.io.Reader in)
|
IProblem |
LecteurDimacs.parseInstance(java.io.Reader input)
|
abstract IProblem |
Reader.parseInstance(java.io.Reader in)
|
IProblem |
AIGReader.parseInstance(java.io.Reader in)
|
IProblem |
InstanceReader.parseInstance(java.lang.String filename)
|
IProblem |
Reader.parseInstance(java.lang.String filename)
|
Uses of IProblem in org.sat4j.specs |
---|
Subinterfaces of IProblem in org.sat4j.specs | |
---|---|
interface |
IOptimizationProblem
Represents an optimization problem. |
interface |
ISolver
This interface contains all services provided by a SAT solver. |
Uses of IProblem in org.sat4j.tools |
---|
Classes in org.sat4j.tools that implement IProblem | |
---|---|
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 |
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 responsabilities to SAT solvers using the Decorator design pattern. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |