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

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<T>
      extended by org.sat4j.tools.xplain.Xplain<T>
Type Parameters:
T - a subinterface to ISolver.
All Implemented Interfaces:
Serializable, IProblem, ISolver, Explainer

public class Xplain<T extends ISolver>
extends SolverDecorator<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

Field Summary
protected  IVecInt assump
           
protected  Map<Integer,IConstr> constrs
           
 
Constructor Summary
Xplain(T solver)
           
Xplain(T solver, boolean skipDuplicatedEntries)
           
 
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.
 IConstr addExactly(IVecInt literals, int n)
          Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
 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[] minimalExplanation()
           
 int[] model()
          Provide a model (if any) for a satisfiable formula.
 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.SolverDecorator
addAllClauses, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, 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,IConstr> constrs

assump

protected IVecInt assump
Constructor Detail

Xplain

public Xplain(T solver,
              boolean skipDuplicatedEntries)

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

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
Specified by:
minimalExplanation in interface Explainer
Throws:
TimeoutException

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)

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.


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.