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

Methods in org.sat4j that return ISolver
protected abstract  ISolver AbstractLauncher.configureSolver(String[] args)
           
protected  ISolver BasicLauncher.configureSolver(String[] args)
           
protected  ISolver MUSLauncher.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)
           
protected  Reader MUSLauncher.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.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.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 ConstraintRelaxingPseudoOptDecorator
           
 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 PseudoBitsAdderDecorator
          A decorator that computes minimal pseudo boolean models.
 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
 BigInteger ObjectiveFunction.calculateDegree(ISolver solver)
           
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 ClausalConstraintsDecorator
           
 class LexicoDecoratorPB
           
 class ManyCorePB
           
 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)
           
 

Constructor parameters in org.sat4j.reader with type arguments of type ISolver
GroupedCNFReader(HighLevelXplain<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 ClausalCardinalitiesDecorator<T extends ISolver>
          A decorator for clausal cardinalities constraints.
 class LexicoDecorator<T extends ISolver>
           
 class ManyCore<S extends ISolver>
           
 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>
           
 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)
           
ModelIterator(ISolver solver, long bound)
           
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 EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
           
 IConstr EncodingStrategyAdapter.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 Policy.addAtMost(ISolver solver, IVecInt literals, int k)
           
 IConstr EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
           
 IConstr Product.addAtMost(ISolver solver, IVecInt literals, int k)
           
 IConstr Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
           
 IConstr Binary.addAtMost(ISolver solver, IVecInt literals, int degree)
           
 IConstr Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
           
 IConstr Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
           
 IConstr Ladder.addAtMostOne(ISolver solver, IVecInt literals)
           
 IConstr EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
           
 IConstr Product.addAtMostOne(ISolver solver, IVecInt literals)
           
 IConstr Commander.addAtMostOne(ISolver solver, IVecInt literals)
          In this encoding, variables are partitioned in groups.
 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 Binomial.addAtMostOne(ISolver solver, IVecInt literals)
           
 IConstr Policy.addExactly(ISolver solver, IVecInt literals, int n)
           
 IConstr EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
           
 IConstr Ladder.addExactlyOne(ISolver solver, IVecInt literals)
           
 IConstr EncodingStrategyAdapter.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 DeletionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
           
 IVecInt InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
           
 

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