org.sat4j.tools
Class SATRaceDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator
      org.sat4j.tools.SATRaceDecorator

All Implemented Interfaces:

java.io.Serializable, IProblem, ISolver

public class SATRaceDecorator
extends SolverDecorator

See Also:

Serialized Form

Constructor Summary

SATRaceDecorator(ISolver solver)

Method Summary

boolean	isSatisfiable() Check the satisfiability of the set of constraints contained inside the solver.
int	newVar(int howmany) Create howmany variables in the solver (and thus in the vocabulary).
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, decorated, getStat, getTimeout, isSatisfiable, model, model, nConstraints, newVar, nVars, printStat, printStat, removeConstr, reset, setTimeout, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SATRaceDecorator

public SATRaceDecorator(ISolver solver)

Method Detail

newVar

public int newVar(int howmany)

Description copied from interface: ISolver

Create howmany variables in the solver (and thus in the vocabulary).

Specified by:

newVar in interface ISolver

Overrides:

newVar in class SolverDecorator

Parameters:

howmany - number of variables to create

Returns:

the total number of variables available in the solver (the highest variable number)

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Description copied from interface: ISolver

To inform the solver of the expected number of clauses to read. This is an optional method, that is called when the p cnf line is read in dimacs formatted input file.

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class SolverDecorator

Parameters:

nb - the expected number of clauses.

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

Returns:

true if the set of constraints is satisfiable, else false.

Throws:

TimeoutException