org.sat4j.opt
Class AbstractSelectorVariablesDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator<ISolver>
      org.sat4j.opt.AbstractSelectorVariablesDecorator

All Implemented Interfaces:

Serializable, IOptimizationProblem, IProblem, ISolver

Direct Known Subclasses:

MaxSatDecorator

public abstract class AbstractSelectorVariablesDecorator
extends SolverDecorator<ISolver>
implements IOptimizationProblem

Abstract class which adds a new "selector" variable for each clause entered in the solver. As a consequence, an original problem with n variables and m clauses will end up with n+m variables.

Author:

daniel

See Also:

Serialized Form

Field Summary

protected int	nbnewvar
protected int	nborigvars
protected boolean[]	prevboolmodel
protected int[]	prevfullmodel
protected int[]	prevmodel

Constructor Summary

AbstractSelectorVariablesDecorator(ISolver solver)

Method Summary

boolean	admitABetterSolution() Look for a solution of the optimization problem.
boolean	admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are satisfied.
int	getExpectedNumberOfClauses()
int[]	model() Provide a model (if any) for a satisfiable formula.
boolean	model(int var) Provide the truth value of a specific variable in the model.
int	newVar(int howmany) Create howmany variables in the solver (and thus in the vocabulary).
void	reset() Clean up the internal state of the solver.
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, addBlockingClause, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, nConstraints, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, 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

Methods inherited from interface org.sat4j.specs.IOptimizationProblem

calculateObjective, discard, discardCurrentSolution, forceObjectiveValueTo, getObjectiveValue, hasNoObjectiveFunction, nonOptimalMeansSatisfiable

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, nVars, printInfos

Field Detail

nborigvars

protected int nborigvars

nbnewvar

protected int nbnewvar

prevfullmodel

protected int[] prevfullmodel

prevmodel

protected int[] prevmodel

Since:

2.1

prevboolmodel

protected boolean[] prevboolmodel

Since:

2.1

Constructor Detail

AbstractSelectorVariablesDecorator

public AbstractSelectorVariablesDecorator(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<ISolver>

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. Note that this method is supposed to be called AFTER a call to newVar(int)

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class SolverDecorator<ISolver>

Parameters:

nb - the expected number of clauses.

See Also:

ISolver.newVar(int)

getExpectedNumberOfClauses

public int getExpectedNumberOfClauses()

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<ISolver>

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem when some literals are satisfied.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Parameters:

assumps - a set of literals in Dimacs format.

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

Since:

2.1

See Also:

ISolver.setTimeout(int)

model

public int[] model()

Description copied from interface: IProblem

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<ISolver>

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

model

public boolean model(int var)

Description copied from interface: IProblem

Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<ISolver>

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

See Also:

IProblem.model()