Package | Description |
---|---|
org.sat4j | |
org.sat4j.minisat.core | |
org.sat4j.opt | |
org.sat4j.pb | |
org.sat4j.pb.core | |
org.sat4j.pb.tools | |
org.sat4j.specs | |
org.sat4j.tools | |
org.sat4j.tools.xplain |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractLauncher.solve(IProblem problem) |
protected void |
AbstractOptimizationLauncher.solve(IProblem problem)
Deprecated.
|
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) |
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) |
Modifier and Type | Method and Description |
---|---|
boolean |
ConstraintRelaxingPseudoOptDecorator.admitABetterSolution() |
boolean |
PseudoOptDecorator.admitABetterSolution() |
boolean |
ConstraintRelaxingPseudoOptDecorator.admitABetterSolution(IVecInt assumps) |
boolean |
PseudoOptDecorator.admitABetterSolution(IVecInt assumps) |
boolean |
ConstraintRelaxingPseudoOptDecorator.isSatisfiable() |
boolean |
OptToPBSATAdapter.isSatisfiable() |
boolean |
PseudoBitsAdderDecorator.isSatisfiable() |
boolean |
PseudoOptDecorator.isSatisfiable() |
boolean |
ConstraintRelaxingPseudoOptDecorator.isSatisfiable(boolean global) |
boolean |
OptToPBSATAdapter.isSatisfiable(boolean global) |
boolean |
PseudoOptDecorator.isSatisfiable(boolean global) |
boolean |
ConstraintRelaxingPseudoOptDecorator.isSatisfiable(IVecInt assumps) |
boolean |
LPStringSolver.isSatisfiable(IVecInt assumps) |
boolean |
OPBStringSolver.isSatisfiable(IVecInt assumps) |
boolean |
OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps) |
boolean |
PseudoBitsAdderDecorator.isSatisfiable(IVecInt assumps) |
boolean |
PseudoOptDecorator.isSatisfiable(IVecInt assumps) |
boolean |
ConstraintRelaxingPseudoOptDecorator.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
LPStringSolver.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
OPBStringSolver.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps,
boolean global) |
boolean |
PseudoOptDecorator.isSatisfiable(IVecInt assumps,
boolean global) |
Modifier and Type | Method and Description |
---|---|
void |
PBSolverCP.analyze(Constr myconfl,
Pair results) |
void |
PBSolverCP.analyzeCP(Constr myconfl,
Pair results) |
int[] |
ObjectiveReducerPBSolverDecorator.findModel() |
int[] |
ObjectiveReducerPBSolverDecorator.findModel(IVecInt assumps) |
boolean |
ObjectiveReducerPBSolverDecorator.isSatisfiable() |
boolean |
ObjectiveReducerPBSolverDecorator.isSatisfiable(boolean globalTimeout) |
boolean |
ObjectiveReducerPBSolverDecorator.isSatisfiable(IVecInt assumps) |
boolean |
ObjectiveReducerPBSolverDecorator.isSatisfiable(IVecInt assumps,
boolean globalTimeout) |
Modifier and Type | Method and Description |
---|---|
boolean |
LexicoDecoratorPB.admitABetterSolution(IVecInt assumps) |
boolean |
SteppedTimeoutLexicoDecoratorPB.admitABetterSolution(IVecInt assumps) |
boolean |
AbstractLexicoHelper.hasASolution() |
boolean |
DependencyHelper.hasASolution() |
boolean |
AbstractLexicoHelper.hasASolution(java.util.Collection<T> assumps) |
boolean |
DependencyHelper.hasASolution(java.util.Collection<T> assumps) |
boolean |
AbstractLexicoHelper.hasASolution(IVec<T> assumps) |
boolean |
DependencyHelper.hasASolution(IVec<T> assumps) |
void |
DependencyHelper.impliedBy(java.util.Collection<T> assumptions,
java.util.Collection<T> satisfied,
java.util.Collection<T> falsified)
Compute the objects implied by the assumptions.
|
java.util.Set<C> |
DependencyHelper.why()
Explain the reason of the inconsistency of the set of constraints.
|
java.util.Set<C> |
DependencyHelper.why(T thing)
Explain a domain object has been set to true in a solution.
|
java.util.Set<C> |
DependencyHelper.whyNot(T thing)
Explain a domain object has been set to false in a solution.
|
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.
|
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[] |
SolverDecorator.findModel() |
int[] |
StatisticsSolver.findModel() |
int[] |
AbstractOutputSolver.findModel(IVecInt assumps) |
int[] |
ManyCore.findModel(IVecInt assumps) |
int[] |
OptToSatAdapter.findModel(IVecInt assumps) |
int[] |
SolverDecorator.findModel(IVecInt assumps) |
int[] |
StatisticsSolver.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 |
ManyCore.isSatisfiable() |
boolean |
ModelIterator.isSatisfiable() |
boolean |
ModelIteratorToSATAdapter.isSatisfiable() |
boolean |
OptToSatAdapter.isSatisfiable() |
boolean |
SolverDecorator.isSatisfiable() |
boolean |
StatisticsSolver.isSatisfiable() |
boolean |
AbstractClauseSelectorSolver.isSatisfiable(boolean global) |
boolean |
AbstractOutputSolver.isSatisfiable(boolean global) |
boolean |
ManyCore.isSatisfiable(boolean globalTimeout) |
boolean |
OptToSatAdapter.isSatisfiable(boolean global) |
boolean |
SolverDecorator.isSatisfiable(boolean global) |
boolean |
StatisticsSolver.isSatisfiable(boolean globalTimeout) |
boolean |
AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps) |
boolean |
AbstractOutputSolver.isSatisfiable(IVecInt assumps) |
boolean |
ManyCore.isSatisfiable(IVecInt assumps) |
boolean |
ModelIterator.isSatisfiable(IVecInt assumps) |
boolean |
ModelIteratorToSATAdapter.isSatisfiable(IVecInt assumps) |
boolean |
OptToSatAdapter.isSatisfiable(IVecInt myAssumps) |
boolean |
SolverDecorator.isSatisfiable(IVecInt assumps) |
boolean |
StatisticsSolver.isSatisfiable(IVecInt assumps) |
boolean |
AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
AbstractOutputSolver.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
ManyCore.isSatisfiable(IVecInt assumps,
boolean globalTimeout) |
boolean |
NegationDecorator.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
OptToSatAdapter.isSatisfiable(IVecInt myAssumps,
boolean global) |
boolean |
SolverDecorator.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
StatisticsSolver.isSatisfiable(IVecInt assumps,
boolean globalTimeout) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.lang.Integer> |
HighLevelXplain.explain() |
java.util.Collection<IConstr> |
Xplain.explain()
Provide an explanation of the inconsistency in term of a subset minimal
set of constraints.
|
IVecInt |
DeletionStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
InsertionStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
MinimizationStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
QuickXplain2001Strategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
IVecInt |
QuickXplainStrategy.explain(ISolver solver,
java.util.Map<java.lang.Integer,?> constrs,
IVecInt assumps) |
int[] |
HighLevelXplain.findModel() |
int[] |
Xplain.findModel() |
int[] |
HighLevelXplain.findModel(IVecInt assumps) |
int[] |
Xplain.findModel(IVecInt assumps) |
boolean |
HighLevelXplain.isSatisfiable() |
boolean |
Xplain.isSatisfiable() |
boolean |
HighLevelXplain.isSatisfiable(boolean global) |
boolean |
Xplain.isSatisfiable(boolean global) |
boolean |
HighLevelXplain.isSatisfiable(IVecInt assumps) |
boolean |
Xplain.isSatisfiable(IVecInt assumps) |
boolean |
HighLevelXplain.isSatisfiable(IVecInt assumps,
boolean global) |
boolean |
Xplain.isSatisfiable(IVecInt assumps,
boolean global) |
int[] |
Explainer.minimalExplanation() |
int[] |
HighLevelXplain.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.
|