org.sat4j.tools
Class SolutionCounter

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by org.sat4j.tools.SolutionCounter
All Implemented Interfaces:
java.io.Serializable, IProblem, ISolver

public class SolutionCounter
extends SolverDecorator<ISolver>

Another solver decorator that counts the number of solutions. Note that this approach is quite naive so do not expect it to work on large examples. The number of solutions will be wrong if the SAT solver does not provide a complete assignment. The class is expected to be used that way:

 SolutionCounter counter = new SolverCounter(SolverFactory.newDefault());
 try {
     int nbSol = counter.countSolutions();
     // the exact number of solutions is nbSol
     ...
  } catch (TimeoutException te) {
     int lowerBound = counter.lowerBound();
     // the solver found lowerBound solutions so far.
     ...
  }
  

Author:
leberre
See Also:
Serialized Form

Constructor Summary
SolutionCounter(ISolver solver)
           
 
Method Summary
 long countSolutions()
          Naive approach to count the solutions available in a boolean formula: each time a solution is found, a new clause is added to prevent it to be found again.
 int lowerBound()
          Get the number of solutions found before the timeout occurs.
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, newVar, nVars, printInfos, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

SolutionCounter

public SolutionCounter(ISolver solver)
Method Detail

lowerBound

public int lowerBound()
Get the number of solutions found before the timeout occurs.

Returns:
the number of solutions found so far.

countSolutions

public long countSolutions()
                    throws TimeoutException
Naive approach to count the solutions available in a boolean formula: each time a solution is found, a new clause is added to prevent it to be found again.

Returns:
the number of solution found.
Throws:
TimeoutException - if the timeout given to the solver is reached.


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