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.xplain   
 

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)
           
 

Methods in org.sat4j that return ISolver
protected abstract  ISolver AbstractLauncher.configureSolver(String[] args)
           
protected  ISolver BasicLauncher.configureSolver(String[] args)
           
 ISolver LightFactory.defaultSolver()
           
 ISolver LightFactory.lightSolver()
           
 

Methods in org.sat4j with parameters of type ISolver
protected abstract  Reader AbstractLauncher.createReader(ISolver theSolver, String problemname)
           
protected  Reader BasicLauncher.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.
 

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
 

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)
           
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)
           
 

Uses of ISolver in org.sat4j.tools
 

Classes in org.sat4j.tools with type parameters of type ISolver
 class SolverDecorator<T extends ISolver>
          The aim of that class is to allow adding dynamic responsabilities to SAT solvers using the Decorator design pattern.
 

Classes in org.sat4j.tools that implement ISolver
 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.
 

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.
 void ConstrGroup.removeFrom(ISolver solver)
           
 

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)
           
ModelIterator(ISolver solver, int bound)
           
SingleSolutionDetector(ISolver solver)
           
SolutionCounter(ISolver solver)
           
 

Uses of ISolver in org.sat4j.tools.xplain
 

Classes in org.sat4j.tools.xplain with type parameters of type ISolver
 class Xplain<T extends ISolver>
          An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
 

Classes in org.sat4j.tools.xplain that implement ISolver
 class Xplain<T extends ISolver>
          An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
 

Methods in org.sat4j.tools.xplain with parameters of type ISolver
 IVecInt QuickXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
           
 IVecInt ReplayXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
           
 IVecInt XplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
           
 



Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.