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

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

Type Parameters:

T - a subinterface to ISolver.

All Implemented Interfaces:

Serializable, IProblem, ISolver

public class Xplain<T extends ISolver>
extends SolverDecorator<T>

An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:

Since:

2.1

Author:

daniel

See Also:

Serialized Form

Field Summary

protected IVecInt	assump
protected Map<Integer,IConstr>	constrs

Constructor Summary

Xplain(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) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
void	cancelExplanation()
protected int	createNewVar(IVecInt literals)
protected void	discardLastestVar()
Collection<IConstr>	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.
Collection<IConstr>	getConstraints()
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[]	model() Provide a model (if any) for a satisfiable formula.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, model, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, 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,IConstr> constrs

assump

protected IVecInt assump

Constructor Detail

Xplain

public Xplain(T solver)

Method Detail

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Description copied from interface: ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).

Specified by:

addClause in interface ISolver

Overrides:

addClause in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals

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 only falsified literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

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

explain

public Collection<IConstr> explain()
                            throws TimeoutException

Returns:

Throws:

TimeoutException

Since:

2.1

cancelExplanation

public void cancelExplanation()

Since:

2.1

getConstraints

public Collection<IConstr> getConstraints()

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)