org.sat4j.tools
Class SingleSolutionDetector

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by 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


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