org.sat4j.pb.core
Class PBSolverWithImpliedClause

java.lang.Object
  org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      org.sat4j.pb.core.PBSolver
          org.sat4j.pb.core.PBSolverCP
              org.sat4j.pb.core.PBSolverWithImpliedClause

All Implemented Interfaces:

Serializable, ICDCL<PBDataStructureFactory>, Learner, UnitPropagationListener, IPBCDCLSolver<PBDataStructureFactory>, IPBSolver, IProblem, ISolver, ISolverService

public class PBSolverWithImpliedClause
extends PBSolverCP

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.pb.core.PBSolver

objectiveFunctionBased, stats

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

constrs, dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, learnedConstraintsDeletionStrategy, learnts, memory_based, NO_SIMPLIFICATION, out, rootLevel, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc

Constructor Summary

PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

Method Summary

IConstr	addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree) Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"
void	claBumpActivity(Constr arg0)
String	toString(String prefix)

Methods inherited from class org.sat4j.pb.core.PBSolverCP

analyze, analyzeCP, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions

Methods inherited from class org.sat4j.pb.core.PBSolver

addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, getObjectiveFunction, setObjectiveFunction

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

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addClause, addConstr, addExactly, analyzeAtRootLevel, analyzeFinalConflictInTermsOfAssumptions, assume, backtrack, cancelUntil, claBumpActivity, clearLearntClauses, currentDecisionLevel, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, fixedSize, getDSFactory, getIthConstr, getLearnedConstraints, getLiteralsPropagatedAt, getLogger, getLogPrefix, getOrder, getOutLearnt, getRestartStrategy, getSearchListener, getSimplifier, getStat, getStats, getTimeout, getTimeoutMs, getVariableHeuristics, getVocabulary, initStats, isDBSimplificationAllowed, isNeedToReduceDB, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, learn, model, model, modelWithInternalVariables, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printLearntClausesInfos, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setLogPrefix, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, simplifyDB, sortOnActivity, stop, suggestNextLiteralToBranchOn, toString, truthValue, undoOne, unsatExplanation, unset, varBumpActivity

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.minisat.core.ICDCL

getLogger, getOrder, getRestartStrategy, getSimplifier, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifier

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos

Methods inherited from interface org.sat4j.minisat.core.UnitPropagationListener

enqueue, enqueue, unset

Methods inherited from interface org.sat4j.minisat.core.VarActivityListener

varBumpActivity

Methods inherited from interface org.sat4j.minisat.core.Learner

learn

Constructor Detail

PBSolverWithImpliedClause

public PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner,
                                 PBDataStructureFactory dsf,
                                 IOrder order)

Method Detail

addPseudoBoolean

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

Description copied from interface: IPBSolver

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

Specified by:

addPseudoBoolean in interface IPBSolver

Overrides:

addPseudoBoolean in class PBSolver

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

toString

public String toString(String prefix)

Specified by:

toString in interface ISolver

Overrides:

toString in class PBSolverCP

claBumpActivity

public void claBumpActivity(Constr arg0)