Uses of Class
org.sat4j.specs.TimeoutException

Packages that use TimeoutException

Package	Description
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

Modifier and Type	Method and Description
protected void	AbstractLauncher.solve(IProblem problem)
protected void	AbstractOptimizationLauncher.solve(IProblem problem) Deprecated.

Uses of TimeoutException in org.sat4j.minisat.core

Methods in org.sat4j.minisat.core that throw TimeoutException

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
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.
static IVecInt	Backbone.compute(ISolver solver) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
static IVecInt	Backbone.compute(ISolver solver, int[] implicant)
static IVecInt	Backbone.compute(ISolver solver, int[] implicant, IVecInt assumptions)
static IVecInt	Backbone.compute(ISolver solver, IVecInt assumptions) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
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[]	OptToSatAdapter.findModel()
int[]	StatisticsSolver.findModel()
int[]	SolverDecorator.findModel()
int[]	AbstractOutputSolver.findModel(IVecInt assumps)
int[]	ManyCore.findModel(IVecInt assumps)
int[]	OptToSatAdapter.findModel(IVecInt assumps)
int[]	StatisticsSolver.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	AbstractClauseSelectorSolver.isSatisfiable()
boolean	AbstractOutputSolver.isSatisfiable()
boolean	ModelIteratorToSATAdapter.isSatisfiable()
boolean	ManyCore.isSatisfiable()
boolean	OptToSatAdapter.isSatisfiable()
boolean	StatisticsSolver.isSatisfiable()
boolean	ModelIterator.isSatisfiable()
boolean	SolverDecorator.isSatisfiable()
boolean	AbstractClauseSelectorSolver.isSatisfiable(boolean global)
boolean	AbstractOutputSolver.isSatisfiable(boolean global)
boolean	ManyCore.isSatisfiable(boolean globalTimeout)
boolean	OptToSatAdapter.isSatisfiable(boolean global)
boolean	StatisticsSolver.isSatisfiable(boolean globalTimeout)
boolean	SolverDecorator.isSatisfiable(boolean global)
boolean	AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps)
boolean	AbstractOutputSolver.isSatisfiable(IVecInt assumps)
boolean	ModelIteratorToSATAdapter.isSatisfiable(IVecInt assumps)
boolean	ManyCore.isSatisfiable(IVecInt assumps)
boolean	OptToSatAdapter.isSatisfiable(IVecInt myAssumps)
boolean	StatisticsSolver.isSatisfiable(IVecInt assumps)
boolean	ModelIterator.isSatisfiable(IVecInt assumps)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps)
boolean	AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	AbstractOutputSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	NegationDecorator.isSatisfiable(IVecInt assumps, boolean global)
boolean	ManyCore.isSatisfiable(IVecInt assumps, boolean globalTimeout)
boolean	OptToSatAdapter.isSatisfiable(IVecInt myAssumps, boolean global)
boolean	StatisticsSolver.isSatisfiable(IVecInt assumps, boolean globalTimeout)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps, boolean global)

Uses of TimeoutException in org.sat4j.tools.xplain

Methods in org.sat4j.tools.xplain that throw TimeoutException

Modifier and Type	Method and Description
Collection<IConstr>	Xplain.explain() Provide an explanation of the inconsistency in term of a subset minimal set of constraints.
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() Provide an explanation of the inconsistency in terms of a subset minimal set of constraints, each constraint being referred to as its index (order) in the solver: first constraint is numbered 1, the second 2, etc.
int[]	HighLevelXplain.minimalExplanation()