Uses of Class
org.sat4j.specs.TimeoutException

Packages that use TimeoutException
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.specs Those classes are intended for users dealing with SAT solvers as black boxes. 
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 AbstractOptimizationLauncher.solve(IProblem problem)
           
protected  void AbstractLauncher.solve(IProblem problem)
           
 

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 MinOneDecorator.admitABetterSolution()
           
 boolean AbstractSelectorVariablesDecorator.admitABetterSolution()
           
 boolean MinOneDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean MaxSatDecorator.admitABetterSolution(IVecInt assumps)
           
 boolean AbstractSelectorVariablesDecorator.admitABetterSolution(IVecInt assumps)
           
 

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[] SolverDecorator.findModel()
           
 int[] ManyCore.findModel()
           
 int[] AbstractOutputSolver.findModel()
           
 int[] SolverDecorator.findModel(IVecInt assumps)
           
 int[] ManyCore.findModel(IVecInt assumps)
           
 int[] AbstractOutputSolver.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 SolverDecorator.isSatisfiable()
           
 boolean OptToSatAdapter.isSatisfiable()
           
 boolean ModelIterator.isSatisfiable()
           
 boolean ManyCore.isSatisfiable()
           
 boolean AbstractOutputSolver.isSatisfiable()
           
 boolean SolverDecorator.isSatisfiable(boolean global)
           
 boolean OptToSatAdapter.isSatisfiable(boolean global)
           
 boolean ManyCore.isSatisfiable(boolean globalTimeout)
           
 boolean AbstractOutputSolver.isSatisfiable(boolean global)
           
 boolean SolverDecorator.isSatisfiable(IVecInt assumps)
           
 boolean OptToSatAdapter.isSatisfiable(IVecInt assumps)
           
 boolean ModelIterator.isSatisfiable(IVecInt assumps)
           
 boolean ManyCore.isSatisfiable(IVecInt assumps)
           
 boolean AbstractOutputSolver.isSatisfiable(IVecInt assumps)
           
 boolean SolverDecorator.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean OptToSatAdapter.isSatisfiable(IVecInt assumps, boolean global)
           
 boolean ManyCore.isSatisfiable(IVecInt assumps, boolean globalTimeout)
           
 boolean AbstractOutputSolver.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 InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
           
 IVecInt DeletionStrategy.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[] Xplain.minimalExplanation()
           
 int[] HighLevelXplain.minimalExplanation()
           
 int[] Explainer.minimalExplanation()
           
 



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