|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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()
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |