Overview  Package  Class   Use  Tree  Deprecated  Index  Help 
 PREV   NEXT FRAMES    NO FRAMES    

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.csp Classes needed for CSP to SAT translation. 
org.sat4j.csp.constraints Classes needed for CSP to SAT translation. 
org.sat4j.csp.encodings   
org.sat4j.maxsat MAXSAT and Weighted Max SAT framework. 
org.sat4j.minisat Implementation of the MiniSAT specification in Java. 
org.sat4j.minisat.core Implementation of the MiniSAT solver skeleton. 
org.sat4j.multicore   
org.sat4j.opt Built-in optimization framework. 
org.sat4j.pb   
org.sat4j.pb.core   
org.sat4j.pb.tools   
org.sat4j.reader Some utility classes to read problems from plain text files. 
org.sat4j.sat   
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.csp
 

Methods in org.sat4j.csp that return ISolver
protected  ISolver CSPLauncher.configureSolver(String[] args)
           
 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.
 

Methods in org.sat4j.csp with parameters of type ISolver
protected  Reader CSPLauncher.createReader(ISolver aSolver, String problemname)
           
 void Encoding.onFinish(ISolver solver, IVec<Var> scope)
           
 void Encoding.onInit(ISolver solver, IVec<Var> scope)
           
 void Encoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void Encoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void Var.toClause(ISolver solver)
           
 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 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.csp.constraints
 

Methods in org.sat4j.csp.constraints with parameters of type ISolver
 void Nogoods.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
           
 void AllDiff.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
           
 void Supports.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
           
 

Uses of ISolver in org.sat4j.csp.encodings
 

Methods in org.sat4j.csp.encodings with parameters of type ISolver
 void GeneralizedSupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
           
 void BinarySupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
           
 void DirectEncoding.onFinish(ISolver solver, IVec<Var> scope)
           
 void GeneralizedSupportEncoding.onInit(ISolver solver, IVec<Var> scope)
           
 void BinarySupportEncoding.onInit(ISolver solver, IVec<Var> scope)
           
 void DirectEncoding.onInit(ISolver solver, IVec<Var> scope)
           
 void GeneralizedSupportEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void BinarySupportEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void DirectEncoding.onNogood(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void GeneralizedSupportEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void BinarySupportEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 void DirectEncoding.onSupport(ISolver solver, IVec<Var> scope, Map<Evaluable,Integer> tuple)
           
 

Uses of ISolver in org.sat4j.maxsat
 

Classes in org.sat4j.maxsat that implement ISolver
 class MinCostDecorator
          A decorator that computes minimal cost models.
 class WeightedMaxSatDecorator
          A decorator for solving weighted MAX SAT problems.
 

Methods in org.sat4j.maxsat that return ISolver
protected  ISolver GenericOptLauncher.configureSolver(String[] args)
           
 

Methods in org.sat4j.maxsat with parameters of type ISolver
protected  Reader GenericOptLauncher.createReader(ISolver aSolver, String problemname)
           
 

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

Classes in org.sat4j.multicore with type parameters of type ISolver
 class ManyCore<S extends ISolver>
           
 

Classes in org.sat4j.multicore that implement ISolver
 class ManyCore<S extends ISolver>
           
 class ManyCorePB
           
 

Methods in org.sat4j.multicore that return ISolver
static ISolver SolverFactory.newManyCore()
           
 

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

Subinterfaces of ISolver in org.sat4j.pb
 interface IPBSolver
          A solver able to deal with pseudo boolean constraints.
 

Classes in org.sat4j.pb that implement ISolver
 class OPBStringSolver
          Solver used to display in a string the pb-instance in OPB format.
 class OptToPBSATAdapter
          Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.
 class PBSolverDecorator
          A decorator for the PB solvers.
 class PseudoIteratorDecorator
          A decorator that computes all pseudo boolean models.
 class PseudoOptDecorator
          A decorator that computes minimal pseudo boolean models.
 class UserFriendlyPBStringSolver<T>
          Solver to display SAT instances using domain objects names instead of Dimacs numbers.
 

Methods in org.sat4j.pb that return ISolver
protected  ISolver LanceurPseudo2007Eclipse.configureSolver(String[] args)
           
protected  ISolver LanceurPseudo2005.configureSolver(String[] args)
           
static ISolver SolverFactory.newDimacsOutput()
           
 

Methods in org.sat4j.pb with parameters of type ISolver
protected  Reader LanceurPseudo2007Eclipse.createReader(ISolver theSolver, String problemname)
           
protected  Reader LanceurPseudo2005.createReader(ISolver theSolver, String problemname)
           
protected  Reader LanceurPseudo2007.createReader(ISolver theSolver, String problemname)
           
 

Uses of ISolver in org.sat4j.pb.core
 

Classes in org.sat4j.pb.core that implement ISolver
 class PBSolver
           
 class PBSolverCautious
           
 class PBSolverClause
           
 class PBSolverCP
           
 class PBSolverMerging
           
 class PBSolverResCP
           
 class PBSolverResolution
           
 class PBSolverWithImpliedClause
           
 

Uses of ISolver in org.sat4j.pb.tools
 

Classes in org.sat4j.pb.tools that implement ISolver
 class XplainPB
           
 

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
CSPExtSupportReader(ISolver solver)
           
CSPInstanceReader(ISolver solver)
           
CSPReader(ISolver solver)
           
CSPSupportReader(ISolver solver)
           
DimacsReader(ISolver solver)
           
DimacsReader(ISolver solver, String format)
           
InstanceReader(ISolver solver)
           
LecteurDimacs(ISolver s)
           
XMLCSPReader(ISolver solver)
           
 

Uses of ISolver in org.sat4j.sat
 

Fields in org.sat4j.sat with type parameters of type ISolver
protected  ASolverFactory<ISolver> Lanceur.factory
           
 

Methods in org.sat4j.sat that return ISolver
protected  ISolver Lanceur.configureSolver(String[] args)
          Configure the solver according to the command line parameters.
 

Methods in org.sat4j.sat with parameters of type ISolver
protected  Reader Lanceur.createReader(ISolver theSolver, String problemname)
           
 

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)
           
 

Overview  Package  Class   Use  Tree  Deprecated  Index  Help 
 PREV   NEXT FRAMES    NO FRAMES    
Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.