org.sat4j.pb.core
Class PBSolver<L extends ILits>

java.lang.Object
  org.sat4j.minisat.core.Solver<L,PBDataStructureFactory<L>>
      org.sat4j.pb.core.PBSolver<L>

All Implemented Interfaces:

java.io.Serializable, Learner, UnitPropagationListener, IPBSolver, IProblem, ISolver

Direct Known Subclasses:

PBSolverCP, PBSolverResolution

public abstract class PBSolver<L extends ILits>
extends Solver<L,PBDataStructureFactory<L>>
implements IPBSolver

See Also:

Serialized Form

Field Summary

protected IVecInt

listOfVariables list of variables for which the solver must provide an explanation for the unsatisfiability if any

Fields inherited from class org.sat4j.minisat.core.Solver

analyzer, dsfactory, EXPENSIVE_SIMPLIFICATION, NO_SIMPLIFICATION, rootLevel, SIMPLE_SIMPLIFICATION, trail, trailLim, voc

Constructor Summary

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L,PBDataStructureFactory<L>> learner, PBDataStructureFactory<L> dsf, IOrder<L> order, RestartStrategy restarter)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L,PBDataStructureFactory<L>> learner, PBDataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter)

Method Summary

IConstr	addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
java.lang.String	getExplanation()
void	setListOfVariablesForExplanation(IVecInt lv)
void	setObjectiveFunction(ObjectiveFunction obj)

Methods inherited from class org.sat4j.minisat.core.Solver

addAllClauses, addAtLeast, addAtMost, addClause, addConstr, analyze, analyzeAtRootLevel, assume, cancelUntil, claBumpActivity, clearLearntClauses, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, getDSFactory, getIthConstr, getOrder, getOutLearnt, getStat, getStats, getTimeout, getTimeoutMs, getVocabulary, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, learn, model, model, nAssigns, nConstraints, newVar, newVar, nVars, printInfos, printLearntClausesInfos, printStat, printStat, propagate, reduceDB, reduceDB, removeConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, simplifyDB, toString, toString, undoOne, varBumpActivity

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addClause, clearLearntClauses, expireTimeout, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, newVar, newVar, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Methods inherited from interface org.sat4j.specs.IProblem

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

Field Detail

listOfVariables

protected IVecInt listOfVariables

list of variables for which the solver must provide an explanation for the unsatisfiability if any

Constructor Detail

PBSolver

public PBSolver(AssertingClauseGenerator acg,
                LearningStrategy<L,PBDataStructureFactory<L>> learner,
                PBDataStructureFactory<L> dsf,
                IOrder<L> order,
                RestartStrategy restarter)

PBSolver

public PBSolver(AssertingClauseGenerator acg,
                LearningStrategy<L,PBDataStructureFactory<L>> learner,
                PBDataStructureFactory<L> dsf,
                SearchParams params,
                IOrder<L> order,
                RestartStrategy restarter)

Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt literals,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger degree)
                         throws ContradictionException

Description copied from interface: IPBSolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:

addPseudoBoolean in interface IPBSolver

Parameters:

literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

moreThan - true if it is a constraint >= degree

degree - the degree of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

setListOfVariablesForExplanation

public void setListOfVariablesForExplanation(IVecInt lv)

Specified by:

setListOfVariablesForExplanation in interface IPBSolver

getExplanation

public java.lang.String getExplanation()

Specified by:

getExplanation in interface IPBSolver

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction obj)

Specified by:

setObjectiveFunction in interface IPBSolver