org.sat4j.tools
Class SolutionCounter

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

All Implemented Interfaces:

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, 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

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.

Since:

2.1

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.