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