Uses of Class
org.sat4j.specs.TimeoutException

Packages that use TimeoutException
org.sat4j Contains a command line launcher for the SAT solvers. 
org.sat4j.maxsat MAXSAT and Weighted Max SAT framework. 
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.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. 
org.sat4j.tools.xplain Implementation of an explanation engine in case of unsatisfiability. 
 

Uses of TimeoutException in org.sat4j
 

Methods in org.sat4j that throw TimeoutException
protected  void AbstractLauncher.solve(IProblem problem)
           
protected  void AbstractOptimizationLauncher.solve(IProblem problem)
           
 

Uses of TimeoutException in org.sat4j.maxsat
 

Methods in org.sat4j.maxsat that throw TimeoutException
 boolean MinCostDecorator.admitABetterSolution()
           
 boolean MinCostDecorator.admitABetterSolution(IVecInt assumps)
           
 

Uses of TimeoutException in org.sat4j.minisat.core
 

Methods in org.sat4j.minisat.core that throw TimeoutException
 void Solver.analyze(Constr confl, Pair results)
           
 int[] Solver.findModel()
           
 int[] Solver.findModel(IVecInt assumps)
           
 boolean Solver.isSatisfiable()
           
 boolean Solver.isSatisfiable(boolean global)
           
 boolean Solver.isSatisfiable(IVecInt assumps)
           
 boolean Solver.isSatisfiable(IVecInt assumps, boolean global)
           
 

Uses of TimeoutException in org.sat4j.opt
 

Methods in org.sat4j.opt that throw TimeoutException
 boolean AbstractSelectorVariablesDecorator.admitABetterSolution()
           
 boolean MinOneDecorator.admitABetterSolution()
           
 boolean AbstractSelectorVariablesDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean MaxSatDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean MinOneDecorator.admitABetterSolution(IVecInt assumps)
           
 

Uses of TimeoutException in org.sat4j.pb
 

Methods in org.sat4j.pb that throw TimeoutException
 boolean ConstraintRelaxingPseudoOptDecorator.admitABetterSolution()
           
 boolean PseudoOptDecorator.admitABetterSolution()
           
 boolean ConstraintRelaxingPseudoOptDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean PseudoOptDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean ConstraintRelaxingPseudoOptDecorator.isSatisfiable()
           
 boolean PseudoOptDecorator.isSatisfiable()
           
 boolean PseudoBitsAdderDecorator.isSatisfiable()
           
 boolean OptToPBSATAdapter.isSatisfiable()
           
 boolean ConstraintRelaxingPseudoOptDecorator.isSatisfiable(boolean global)
           
 boolean PseudoOptDecorator.isSatisfiable(boolean global)
           
 boolean OptToPBSATAdapter.isSatisfiable(boolean global)
           
 boolean ConstraintRelaxingPseudoOptDecorator.isSatisfiable(IVecInt assumps)
           
 boolean PseudoOptDecorator.isSatisfiable(IVecInt assumps)
           
 boolean PseudoBitsAdderDecorator.isSatisfiable(IVecInt assumps)
           
 boolean OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps)
           
 boolean OPBStringSolver.isSatisfiable(IVecInt assumps)
           
 boolean ConstraintRelaxingPseudoOptDecorator.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean PseudoOptDecorator.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps, boolean global)
           
 boolean OPBStringSolver.isSatisfiable(IVecInt assumps, boolean global)
           
 

Uses of TimeoutException in org.sat4j.pb.core
 

Methods in org.sat4j.pb.core that throw TimeoutException
 void PBSolverCP.analyze(Constr myconfl, Pair results)
           
 void PBSolverCP.analyzeCP(Constr myconfl, Pair results)
           
 

Uses of TimeoutException in org.sat4j.pb.tools
 

Methods in org.sat4j.pb.tools that throw TimeoutException
 boolean LexicoDecoratorPB.admitABetterSolution(IVecInt assumps)
           
 boolean DependencyHelper.hasASolution()
           
 boolean DependencyHelper.hasASolution(Collection<T> assumps)
           
 boolean DependencyHelper.hasASolution(IVec<T> assumps)
           
 Set<C> DependencyHelper.why()
          Explain the reason of the inconsistency of the set of constraints.
 Set<C> DependencyHelper.why(T thing)
          Explain a domain object has been set to true in a solution.
 Set<C> DependencyHelper.whyNot(T thing)
          Explain a domain object has been set to false in a solution.
 

Uses of TimeoutException in org.sat4j.specs
 

Methods in org.sat4j.specs that throw TimeoutException
 boolean IOptimizationProblem.admitABetterSolution()
          Look for a solution of the optimization problem.
 boolean IOptimizationProblem.admitABetterSolution(IVecInt assumps)
          Look for a solution of the optimization problem when some literals are satisfied.
 int[] IProblem.findModel()
          Look for a model satisfying all the clauses available in the problem.
 int[] IProblem.findModel(IVecInt assumps)
          Look for a model satisfying all the clauses available in the problem.
 boolean IProblem.isSatisfiable()
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean IProblem.isSatisfiable(boolean globalTimeout)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean IProblem.isSatisfiable(IVecInt assumps)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean IProblem.isSatisfiable(IVecInt assumps, boolean globalTimeout)
          Check the satisfiability of the set of constraints contained inside the solver.
 

Uses of TimeoutException in org.sat4j.tools
 

Methods in org.sat4j.tools that throw TimeoutException
 boolean LexicoDecorator.admitABetterSolution()
           
 boolean LexicoDecorator.admitABetterSolution(IVecInt assumps)
           
static IVecInt RemiUtils.backbone(ISolver s)
          Compute the set of literals common to all models of the formula.
 long SolutionCounter.countSolutions()
          Naive approach to count the solutions available in a boolean formula: each time a solution is found, a new clause is added to prevent it to be found again.
 int[] AbstractOutputSolver.findModel()
           
 int[] ManyCore.findModel()
           
 int[] SolverDecorator.findModel()
           
 int[] AbstractOutputSolver.findModel(IVecInt assumps)
           
 int[] ManyCore.findModel(IVecInt assumps)
           
 int[] SolverDecorator.findModel(IVecInt assumps)
           
 boolean SingleSolutionDetector.hasASingleSolution()
          Please use that method only after a positive answer from isSatisfiable() (else a runtime exception will be launched).
 boolean SingleSolutionDetector.hasASingleSolution(IVecInt assumptions)
          Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).
 boolean AbstractOutputSolver.isSatisfiable()
           
 boolean ManyCore.isSatisfiable()
           
 boolean OptToSatAdapter.isSatisfiable()
           
 boolean ModelIterator.isSatisfiable()
           
 boolean SolverDecorator.isSatisfiable()
           
 boolean AbstractOutputSolver.isSatisfiable(boolean global)
           
 boolean ManyCore.isSatisfiable(boolean globalTimeout)
           
 boolean OptToSatAdapter.isSatisfiable(boolean global)
           
 boolean SolverDecorator.isSatisfiable(boolean global)
           
 boolean AbstractOutputSolver.isSatisfiable(IVecInt assumps)
           
 boolean ManyCore.isSatisfiable(IVecInt assumps)
           
 boolean OptToSatAdapter.isSatisfiable(IVecInt assumps)
           
 boolean ModelIterator.isSatisfiable(IVecInt assumps)
           
 boolean SolverDecorator.isSatisfiable(IVecInt assumps)
           
 boolean AbstractOutputSolver.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean ManyCore.isSatisfiable(IVecInt assumps, boolean globalTimeout)
           
 boolean OptToSatAdapter.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean SolverDecorator.isSatisfiable(IVecInt assumps, boolean global)
           
 

Uses of TimeoutException in org.sat4j.tools.xplain
 

Methods in org.sat4j.tools.xplain that throw TimeoutException
 Collection<IConstr> Xplain.explain()
           
 Collection<Integer> HighLevelXplain.explain()
           
 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)
           
 int[] Xplain.findModel()
           
 int[] HighLevelXplain.findModel()
           
 int[] Xplain.findModel(IVecInt assumps)
           
 int[] HighLevelXplain.findModel(IVecInt assumps)
           
 boolean Xplain.isSatisfiable()
           
 boolean HighLevelXplain.isSatisfiable()
           
 boolean Xplain.isSatisfiable(boolean global)
           
 boolean HighLevelXplain.isSatisfiable(boolean global)
           
 boolean Xplain.isSatisfiable(IVecInt assumps)
           
 boolean HighLevelXplain.isSatisfiable(IVecInt assumps)
           
 boolean Xplain.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean HighLevelXplain.isSatisfiable(IVecInt assumps, boolean global)
           
 int[] Explainer.minimalExplanation()
           
 int[] Xplain.minimalExplanation()
           
 int[] HighLevelXplain.minimalExplanation()
           
 



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