|
||||||||||
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 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 |
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 | |
---|---|
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 | |
---|---|
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[] |
DimacsOutputSolver.findModel()
|
int[] |
DimacsStringSolver.findModel()
|
int[] |
SolverDecorator.findModel()
|
int[] |
DimacsOutputSolver.findModel(IVecInt assumps)
|
int[] |
DimacsStringSolver.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 |
DimacsOutputSolver.isSatisfiable()
|
boolean |
OptToSatAdapter.isSatisfiable()
|
boolean |
DimacsStringSolver.isSatisfiable()
|
boolean |
ModelIterator.isSatisfiable()
|
boolean |
SolverDecorator.isSatisfiable()
|
boolean |
DimacsOutputSolver.isSatisfiable(boolean global)
|
boolean |
OptToSatAdapter.isSatisfiable(boolean global)
|
boolean |
DimacsStringSolver.isSatisfiable(boolean global)
|
boolean |
SolverDecorator.isSatisfiable(boolean global)
|
boolean |
DimacsOutputSolver.isSatisfiable(IVecInt assumps)
|
boolean |
OptToSatAdapter.isSatisfiable(IVecInt assumps)
|
boolean |
DimacsStringSolver.isSatisfiable(IVecInt assumps)
|
boolean |
ModelIterator.isSatisfiable(IVecInt assumps)
|
boolean |
SolverDecorator.isSatisfiable(IVecInt assumps)
|
boolean |
DimacsOutputSolver.isSatisfiable(IVecInt assumps,
boolean global)
|
boolean |
OptToSatAdapter.isSatisfiable(IVecInt assumps,
boolean global)
|
boolean |
DimacsStringSolver.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()
|
IVecInt |
QuickXplainStrategy.explain(ISolver solver,
Map<Integer,IConstr> constrs,
IVecInt assumps)
|
IVecInt |
ReplayXplainStrategy.explain(ISolver solver,
Map<Integer,IConstr> constrs,
IVecInt assumps)
|
IVecInt |
XplainStrategy.explain(ISolver solver,
Map<Integer,IConstr> constrs,
IVecInt assumps)
|
int[] |
Xplain.findModel()
|
int[] |
Xplain.findModel(IVecInt assumps)
|
boolean |
Xplain.isSatisfiable()
|
boolean |
Xplain.isSatisfiable(boolean global)
|
boolean |
Xplain.isSatisfiable(IVecInt assumps)
|
boolean |
Xplain.isSatisfiable(IVecInt assumps,
boolean global)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |