org.sat4j.tools
Class SingleSolutionDetector

java.lang.Object
  org.sat4j.tools.SolverDecorator<ISolver>
      org.sat4j.tools.SingleSolutionDetector

All Implemented Interfaces:

Serializable, IProblem, ISolver

public class SingleSolutionDetector
extends SolverDecorator<ISolver>

This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not. NOTE THAT THIS DECORATOR CANNOT BE USED WITH SOLVERS USING SPECIFIC DATA STRUCTURES FOR BINARY OR TERNARY CLAUSES! SingleSolutionDetector problem = new SingleSolutionDetector(SolverFactory.newMiniSAT()); // feed problem/solver as usual if (problem.isSatisfiable()) { if (problem.hasASingleSolution()) { // great, the instance has a unique solution int [] uniquesolution = problem.getModel(); } else { // too bad, got more than one } }

Author:

leberre

See Also:

Serialized Form

Constructor Summary

SingleSolutionDetector(ISolver solver)

Method Summary

boolean	hasASingleSolution() Please use that method only after a positive answer from isSatisfiable() (else a runtime exception will be launched).
boolean	hasASingleSolution(IVecInt assumptions) Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, 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

Constructor Detail

SingleSolutionDetector

public SingleSolutionDetector(ISolver solver)

Method Detail

hasASingleSolution

public boolean hasASingleSolution()
                           throws TimeoutException

Please use that method only after a positive answer from isSatisfiable() (else a runtime exception will be launched). NOTE THAT THIS FUNCTION SHOULD NOT ONLY BE USED ONCE THE FINAL SOLUTION IS FOUND, SINCE THE METHOD ADDS CONSTRAINTS INTO THE SOLVER THAT MAY NOT BE REMOVED UNDER CERTAIN CONDITIONS (UNIT CONSTRAINTS LEARNT FOR INSTANCE). THAT ISSUE WILL BE RESOLVED ONCE REMOVECONSTR WILL WORK PROPERLY.

Returns:

true iff there is only one way to satisfy all the constraints in the solver.

Throws:

TimeoutException

See Also:

ISolver#removeConstr(IConstr)}

hasASingleSolution

public boolean hasASingleSolution(IVecInt assumptions)
                           throws TimeoutException

Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).

Parameters:

assumptions - a set of literals (dimacs numbering) that must be satisfied.

Returns:

true iff there is only one way to satisfy all the constraints in the solver using the provided set of assumptions.

Throws:

TimeoutException