org.sat4j.tools.xplain

Class Xplain<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.AbstractClauseSelectorSolver<T>

org.sat4j.tools.FullClauseSelectorSolver<T>

org.sat4j.tools.xplain.Xplain<T>

Type Parameters:

T - a subinterface to ISolver.

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel, Explainer

public class Xplain<T extends ISolver>
extends FullClauseSelectorSolver<T>
implements Explainer

Explanation framework for SAT4J. The explanation uses selector variables and assumptions. It is based on a two steps method: 1) extraction of a set of assumptions implying the inconsistency 2) minimization of that set.

Since:

2.1

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
Xplain(T solver)
Xplain(T solver, boolean skipDuplicatedEntries)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtLeast(IVecInt literals, int degree) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	addAtMost(IVecInt literals, int degree) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
void	cancelExplanation()
Collection<IConstr>	explain() Provide an explanation of the inconsistency in term of a subset minimal set of constraints.
int[]	findModel() Look for a model satisfying all the clauses available in the problem.
int[]	findModel(IVecInt assumps) Look for a model satisfying all the clauses available in the problem.
boolean	isSatisfiable() Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(boolean global) Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(IVecInt assumps) Check the satisfiability of the set of constraints contained inside the solver.
boolean	isSatisfiable(IVecInt assumps, boolean global) Check the satisfiability of the set of constraints contained inside the solver.
int[]	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.
boolean	removeConstr(IConstr c) Remove a constraint returned by one of the add method from the solver.
boolean	removeSubsumedConstr(IConstr c) Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.
void	setMinimizationStrategy(MinimizationStrategy strategy)
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.tools.FullClauseSelectorSolver

addClause, addControlableClause, addNonControlableClause, getAddedVars, getConstraints, getConstrs, getLastClause, getLastConstr, isSkipDuplicatedEntries, model, setLastConstr

Methods inherited from class org.sat4j.tools.AbstractClauseSelectorSolver

createNewVar, discardLastestVar, externalState, internalState

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, toString, unsatExplanation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Xplain

public Xplain(T solver,
      boolean skipDuplicatedEntries)

Xplain

public Xplain(T solver)

Method Detail

addExactly

public IConstr addExactly(IVecInt literals,
                 int n)
                   throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "exactly n of those literals must be satisfied".

Specified by:

addExactly in interface ISolver

Overrides:

addExactly in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

n - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                 int degree)
                   throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Specified by:

addAtLeast in interface ISolver

Overrides:

addAtLeast in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if degree literals are not remaining unfalsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addAtMost

public IConstr addAtMost(IVecInt literals,
                int degree)
                  throws ContradictionException

Description copied from interface: ISolver

Create a cardinality constraint of the type "at most n of those literals must be satisfied"

Specified by:

addAtMost in interface ISolver

Overrides:

addAtMost in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.

degree - the degree (n) of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if it contains more than degree satisfied literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

minimalExplanation

public int[] minimalExplanation()
                         throws TimeoutException

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.

Specified by:

minimalExplanation in interface Explainer

Returns:

an array of indexes such that the set of indexed constraints is inconsistent.

Throws:

TimeoutException

See Also:

#explain()}

explain

public Collection<IConstr> explain()
                            throws TimeoutException

Provide an explanation of the inconsistency in term of a subset minimal set of constraints. Compared to minimalExplanation(), the method returns a reference to the constraint object, instead of an index.

Returns:

Throws:

TimeoutException

Since:

2.1

See Also:

#minimalExplanation()}

cancelExplanation

public void cancelExplanation()

Since:

2.1

findModel

public int[] findModel()
                throws TimeoutException

Description copied from interface: IProblem

Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable() and model() methods, as shown in the pseudo-code: if (isSatisfiable()) { return model(); } return null;

Specified by:

findModel in interface IProblem

Overrides:

findModel in class SolverDecorator<T extends ISolver>

Returns:

a model of the formula as an array of literals to satisfy, or null if no model is found

Throws:

TimeoutException - if a model cannot be found within the given timeout.

findModel

public int[] findModel(IVecInt assumps)
                throws TimeoutException

Description copied from interface: IProblem

Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable(IVecInt) and model() methods, as shown in the pseudo-code: if (isSatisfiable(assumpt)) { return model(); } return null;

Specified by:

findModel in interface IProblem

Overrides:

findModel in class SolverDecorator<T extends ISolver>

Returns:

a model of the formula as an array of literals to satisfy, or null if no model is found

Throws:

TimeoutException - if a model cannot be found within the given timeout.

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class AbstractClauseSelectorSolver<T extends ISolver>

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class AbstractClauseSelectorSolver<T extends ISolver>

Parameters:

global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class AbstractClauseSelectorSolver<T extends ISolver>

Parameters:

assumps - a set of literals (represented by usual non null integers in Dimacs format).

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps,
                    boolean global)
                      throws TimeoutException

Description copied from interface: IProblem

Check the satisfiability of the set of constraints contained inside the solver.

Specified by:

isSatisfiable in interface IProblem

Overrides:

isSatisfiable in class AbstractClauseSelectorSolver<T extends ISolver>

Parameters:

assumps - a set of literals (represented by usual non null integers in Dimacs format).

global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.

Returns:

true if the set of constraints is satisfiable when literals are satisfied, else false.

Throws:

TimeoutException

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class SolverDecorator<T extends ISolver>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

setMinimizationStrategy

public void setMinimizationStrategy(MinimizationStrategy strategy)

Specified by:

setMinimizationStrategy in interface Explainer

removeConstr

public boolean removeConstr(IConstr c)

Description copied from interface: ISolver

Remove a constraint returned by one of the add method from the solver. All learned clauses will be cleared. Current implementation does not handle properly the case of unit clauses.

Specified by:

removeConstr in interface ISolver

Overrides:

removeConstr in class SolverDecorator<T extends ISolver>

Parameters:

c - a constraint returned by one of the add method.

Returns:

true if the constraint was successfully removed.

removeSubsumedConstr

public boolean removeSubsumedConstr(IConstr c)

Description copied from interface: ISolver

Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver. Unlike the removeConstr() method, learned clauses will NOT be cleared. That method is expected to be used to remove constraints used in the optimization process. In order to prevent a wrong from the user, the method will only work if the argument is the last constraint added to the solver. An illegal argument exception will be thrown in other cases.

Specified by:

removeSubsumedConstr in interface ISolver

Overrides:

removeSubsumedConstr in class SolverDecorator<T extends ISolver>

Parameters:

c - a constraint returned by one of the add method. It must be the latest constr added to the solver.

Returns:

true if the constraint was successfully removed.