Uses of Interface
org.sat4j.specs.IProblem

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.
 



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