org.sat4j.tools.xplain
Class HighLevelXplain<T extends ISolver>

java.lang.Object
  org.sat4j.tools.SolverDecorator<T>
      org.sat4j.tools.xplain.HighLevelXplain<T>

Type Parameters:

T - a subinterface to ISolver.

All Implemented Interfaces:

Serializable, IProblem, ISolver, Explainer

public class HighLevelXplain<T extends ISolver>
extends SolverDecorator<T>
implements Explainer

Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.

Since:

2.1

Author:

daniel

See Also:

Serialized Form

Field Summary

protected IVecInt	assump
protected Map<Integer,Integer>	constrs

Constructor Summary

HighLevelXplain(T solver)

Method Summary

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	addClause(IVecInt literals, int desc)
void	cancelExplanation()
protected int	createNewVar(IVecInt literals)
protected void	discardLastestVar()
Collection<Integer>	explain()
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()
int[]	model() Provide a model (if any) for a satisfiable formula.
void	setMinimizationStrategy(MinimizationStrategy strategy)
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.tools.SolverDecorator

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

Methods inherited from class java.lang.Object

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

Field Detail

constrs

protected Map<Integer,Integer> constrs

assump

protected IVecInt assump

Constructor Detail

HighLevelXplain

public HighLevelXplain(T solver)

Method Detail

addClause

public IConstr addClause(IVecInt literals,
                         int desc)
                  throws ContradictionException

Parameters:

literals - a clause

desc - the level of the clause set

Returns:

on object representing that clause in the solver.

Throws:

ContradictionException

createNewVar

protected int createNewVar(IVecInt literals)

Parameters:

literals -

Returns:

Since:

2.1

discardLastestVar

protected void discardLastestVar()

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

Specified by:

minimalExplanation in interface Explainer

Throws:

TimeoutException

explain

public Collection<Integer> explain()
                            throws TimeoutException

Returns:

Throws:

TimeoutException

Since:

2.1

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 SolverDecorator<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 SolverDecorator<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 SolverDecorator<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 SolverDecorator<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

model

public int[] model()

Description copied from interface: IProblem

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<T extends ISolver>

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

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