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

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)


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